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

improve comments for math_paper, eliminated unnecessary comments in ML
HOL-OCL/Isabelle_DOF/master This commit looks good Details

This commit is contained in:
Burkhart Wolff 2019-01-11 15:01:34 +01:00
parent 12dd12a070
commit fbf28d4db7
2 changed files with 7 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
examples/conceptual/AssnsLemmaThmEtc.thy
View File

@ -23,6 +23,7 @@ assert*[aa::F] "True"
ML\<open>assert_list_dest @{docitem_attribute property :: aa}\<close>
assert*[aa::F] "True & True" (* small pb: unicodes crashes here ... *)
ML\<open> assert_list_dest @{docitem_attribute property :: aa}\<close>
(* bigger pb: overrides last solution ... *)
text\<open>An example for the ontology specification character of the short-cuts such as
@{command "assert*"}: in the following, we use the same notation referring to a completely

9
ontologies/math_paper.thy
View File

@ -2,9 +2,12 @@ chapter \<open>The Document Ontology Common Library for the Isabelle Ontology Fr
text\<open> Offering support for common Isabelle Elements like definitions, lemma- and theorem
statements, proofs, etc. Isabelle is a lot of things, but it is an interactive theorem
proving environment after all !
\<^item>
\<^item>
proving environment after all ! So this ontology provides:
\<^item> declarations for textual descriptions of definitions, lemmas, theorems, assertions, ...
and the usual means for typed referencing on them,
\<^item> monitors allowing for filtering content; this means (typed) brackets that can be
put around formal content that is more or less relevant for different types of users,
\fixme{find nicer formulation}
\<^item> LaTeX support. \<close>