diff --git a/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy b/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy index 69d6590..f6f255a 100644 --- a/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy +++ b/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy @@ -680,7 +680,7 @@ typ\\test_G.tag_attribute :: int\\ text*[xcv6::"\test_G.tag_attribute :: int\ test_F", b="{(@{test_A ''xcv3''},@{test_G ''xcv5''})}"]\\ -text\\lemma*\, etc. do not support well polymorphic classes. +text\\lemma*\, etc. do not support well polymorphic classes term antiquotations. For now only embedded term-antiquotation in a definition could work:\ definition* testtest_level where "testtest_level \ the (text_section.level @{test2 \testtest2''\})" lemma*[e5::E] testtest : "xx + testtest_level = yy + testtest_level \ xx = yy" by simp