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

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

This commit is contained in:
Burkhart Wolff 2019-02-08 15:43:49 +01:00
parent 8fff0730d6
commit 65346b3f0a
1 changed files with 6 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
examples/conceptual/Attributes.thy
View File

@ -17,6 +17,12 @@ Symtab.dest docitem_tab;
Symtab.dest docclass_tab;
\<close>
ML\<open>
fun fac x = if x = 0 then 1 else x * (fac(x -1));
fac 3;
open Thm;
\<close>
text\<open>A text item containing standard theorem antiquotations and complex meta-information.\<close>
text*[dfgdfg::B, Conceptual.B.x ="''f''", y = "[''sdf'']"]\<open> Lorem ipsum ... @{thm refl} \<close>