diff --git a/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy b/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy index 0814421..412ee88 100644 --- a/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy +++ b/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy @@ -701,16 +701,16 @@ aaa::"'a list" doc_class 'a BBB_test = bbb::"'a list" -declare_reference*[aaa_test::"'a::one AAA"] -text\@{AAA (unchecked) \aaa_test\}\ +declare_reference*[aaa_test::"'a::one AAA_test"] +text\@{AAA_test (unchecked) \aaa_test\}\ text\bbb_test should fails and trigger an error \ -text*[bbb_test::"'a::one BBB"]\\ +text*[bbb_test::"'a::one BBB_test"]\\ -text*[aaa_test::"int AAA"]\\ +text*[aaa_test::"int AAA_test"]\\ text\bbb_test should fails and trigger an error \ -text*[aaa_test'::"string AAA"]\\ +text*[aaa_test'::"string AAA_test"]\\ end \ No newline at end of file