2018-12-19 11:05:57 +00:00
|
|
|
theory AssnsLemmaThmEtc
|
|
|
|
|
imports "../../ontologies/Conceptual" "../../ontologies/math_paper"
|
|
|
|
|
begin
|
|
|
|
|
|
|
|
|
|
section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>
|
|
|
|
|
|
|
|
|
|
text\<open>Current status:\<close>
|
|
|
|
|
print_doc_classes
|
|
|
|
|
print_doc_items
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
section\<open>Definitions, Lemmas, Theorems, Assertions\<close>
|
|
|
|
|
(* auxilliary *)
|
|
|
|
|
ML\<open>fun assert_list_dest X = map HOLogic.dest_string
|
|
|
|
|
(map (fn Const ("Isa_DOF.ISA_term", _) $ s => s )
|
|
|
|
|
(HOLogic.dest_list X))\<close>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
text*[aa::F]\<open>Our definition of the HOL-Logic has the following properties:\<close>
|
|
|
|
|
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>
|
2019-01-11 14:01:34 +00:00
|
|
|
(* bigger pb: overrides last solution ... *)
|
2018-12-19 11:05:57 +00:00
|
|
|
|
|
|
|
|
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
|
|
|
|
|
different class. "F" and "assertion" have only in common that they posses the attribute
|
|
|
|
|
\<^verbatim>\<open>property\<close>: \<close>
|
|
|
|
|
|
|
|
|
|
text*[aaa::assertion]\<open>Our definition of the integers has the following properties:\<close>
|
|
|
|
|
assert*[aaa::assertion] "3 < (4::int)"
|
|
|
|
|
assert*[aaa::assertion] "0 < (4::int)"
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
end
|
|
|
|
|
(*>*)
|
