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

Diverses

This commit is contained in:
Burkhart Wolff 2018-04-08 11:29:59 +02:00
parent 3cf86c2d32
commit 64a1c82242
2 changed files with 13 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
examples/cenelec/Example.thy
View File

@ -25,7 +25,7 @@ text*[tralala] {* Brexit means Brexit *}
text*[ass1::assumption] {* Brexit means Brexit *}
text*[hyp1::hypothesis] {* P means not P *}
text*[hyp1::hypothesis] {* P inequal NP *}
text*[ass122::srac] {* The overall sampling frequence of the odometer
@ -39,7 +39,7 @@ to a test-environment or test-engine *}
text \<open> As established by @{docref (unchecked) \<open>t10\<close>},
@{docref (define) \<open>t10\<close>} \<close>
text \<open> the @{docref \<open>t10\<close>}
text \<open> the @{docref \<open>t10\<close>}
the @{docref \<open>ass122\<close>}
\<close>
text \<open> safety related applicability condition @{srac \<open>ass122\<close>}. \<close>

12
examples/simple/Article.thy
View File

@ -31,7 +31,17 @@ sed nibh ut lorem integer, maecenas sed mi purus non nunc, morbi pretium tortor.
section*[bgrnd::text_section]{* Background: Isabelle and Isabelle_DOF *}
text{* As mentioned in @{introduction \<open>intro\<close>} ... *}
update_instance*[bgrnd, main_author = "Some(''bu'')"]
term "a + b = b + a"
(*
@{term ''a + b = b + a''}
@{typ ''a list''}
@{thm ''refl''}
@{thms ''[refl,sym]''}
*)
update_instance*[bgrnd, main_author = "Some(''bu'')", formula="@{term ''a + b = b + a''}"]
section*[ontomod::technical]{* Modeling Ontologies in Isabelle_DOF *}
text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi,*}