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

petitesse
HOL-OCL/Isabelle_DOF/master This commit looks good Details

This commit is contained in:
Burkhart Wolff 2019-04-19 16:16:54 +02:00
parent 76f86c5c0e
commit b035996d36
1 changed files with 5 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
ontologies/CENELEC_50128.thy
View File

@ -734,5 +734,10 @@ Syntax.read_typ @{context} "hypothesis" handle _ => dummyT;
Proof_Context.init_global;
\<close>
text\<open>
@{theory_text [display] \<open>definition a\<^sub>E \<equiv> True
lemma XXX : "True = False " by auto\<close>}
\<close>
end