Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Update bug example in Test_Polymorphic_Classes

This commit is contained in:
Nicolas Méric 2024-03-04 14:32:46 +01:00
parent 42da18cf3a
commit 46b094939a
1 changed files with 5 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy
View File

@ -701,16 +701,16 @@ aaa::"'a list"
doc_class 'a BBB_test =
bbb::"'a list"
declare_reference*[aaa_test::"'a::one AAA"]
text\<open>@{AAA (unchecked) \<open>aaa_test\<close>}\<close>
declare_reference*[aaa_test::"'a::one AAA_test"]
text\<open>@{AAA_test (unchecked) \<open>aaa_test\<close>}\<close>
text\<open>bbb_test should fails and trigger an error \<close>
text*[bbb_test::"'a::one BBB"]\<open>\<close>
text*[bbb_test::"'a::one BBB_test"]\<open>\<close>
text*[aaa_test::"int AAA"]\<open>\<close>
text*[aaa_test::"int AAA_test"]\<open>\<close>
text\<open>bbb_test should fails and trigger an error \<close>
text*[aaa_test'::"string AAA"]\<open>\<close>
text*[aaa_test'::"string AAA_test"]\<open>\<close>
end