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

...

This commit is contained in:
Burkhart Wolff 2022-03-31 10:12:46 +02:00
parent 6a7b5c6afb
commit a68ecb4f11
1 changed files with 3 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/tests/Evaluation.thy
View File

@ -62,13 +62,11 @@ text\<open>Now we can evaluate a term with TA:
the current implementation return the term which references the object referenced by the TA.
Here the evualuation of the TA will return the HOL.String which references the theorem:
\<close>
value*\<open>@{thm \<open>HOL.refl\<close>}\<close>
value*\<open>@{thm \<open>HOL.refl\<close>}\<close> \<comment> \<open>syntax check\<close>
value*[axxx::A]\<open>@{thm \<open>HOL.refl\<close>}\<close> (* using the option *)
value*[axxx::A]\<open>@{thm \<open>HOL.refl\<close>}\<close> \<comment> \<open>defining a reference of class A\<close>
value*[axxxx::A]\<open>@{thm \<open>HOL.refl\<close>}\<close>
text\<open>check : @{A [display] "axxx"}\<close>
text\<open>check : @{A [display] "axxx"}\<close> \<comment> \<open>using it\<close>
text\<open>An instance class is an object which allows us to define the concepts we want in an ontology.
It is a concept which will be used to implement an ontology. It has roughly the same meaning as