From 43aad517b9427239fa6774e9e99a1cc2a851e492 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= <nicolasmeric@posteo.net>
Date: Thu, 20 Jul 2023 16:25:25 +0200
Subject: [PATCH] Add basic explanation for lemma*, etc.

Add basic explanation how to use lemma*, etc.
with term antiquotations of polymorphic class instances
---
 Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy b/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy
index 8f46155..69d6590 100644
--- a/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy
+++ b/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy
@@ -679,4 +679,13 @@ typ\<open>unit test_G_ext\<close>
 typ\<open>\<lparr>test_G.tag_attribute :: int\<rparr>\<close>
 text*[xcv6::"\<lparr>test_G.tag_attribute :: int\<rparr> test_F", b="{(@{test_A ''xcv3''},@{test_G ''xcv5''})}"]\<open>\<close>
 
+
+text\<open>\<open>lemma*\<close>, etc. do not support well polymorphic classes.
+For now only embedded term-antiquotation in a definition could work:\<close>
+definition* testtest_level where "testtest_level \<equiv> the (text_section.level @{test2 \<open>testtest2''\<close>})"
+lemma*[e5::E] testtest : "xx + testtest_level = yy + testtest_level \<Longrightarrow> xx = yy" by simp
+
+text\<open>Indeed this fails:\<close>
+(*lemma*[e6::E] testtest : "xx + the (level @{test2 \<open>testtest2''\<close>}) = yy + the (level @{test2 \<open>testtest2''\<close>}) \<Longrightarrow> xx = yy" by simp*)
+
 end
\ No newline at end of file