2018-09-06 10:07:37 +00:00
|
|
|
theory InnerSyntaxAntiquotations
|
|
|
|
imports "../../ontologies/Conceptual"
|
|
|
|
begin
|
|
|
|
|
2018-09-17 14:58:38 +00:00
|
|
|
ML\<open> val ({tab = x, ...},y,z)= DOF_core.get_data @{context}; Symtab.dest z; \<close>
|
2018-09-06 10:07:37 +00:00
|
|
|
|
2018-09-11 11:51:25 +00:00
|
|
|
lemma murks : "T = {ert,dfg}" sorry
|
|
|
|
|
2018-09-17 14:58:38 +00:00
|
|
|
text\<open>Example for a meta-attribute of ODL-type @{typ "file"} with an appropriate ISA for the
|
|
|
|
file @{file "./Attributes.thy"}\<close>
|
2018-09-06 10:07:37 +00:00
|
|
|
text*[xcv::F, u="@{file ''./examples/conceptual/Attributes.thy''}"]\<open>Lorem ipsum ...\<close>
|
|
|
|
|
2018-09-17 14:48:05 +00:00
|
|
|
text*[xcv1::A, x=5]\<open>Lorem ipsum ...\<close>
|
|
|
|
text*[xcv3::A, x=7]\<open>Lorem ipsum ...\<close>
|
2018-09-17 14:58:38 +00:00
|
|
|
|
|
|
|
text\<open>Example for a meta-attribute of ODL-type @{typ "typ"} with an appropriate ISA for the
|
|
|
|
theorem @{thm "refl"}}\<close>
|
|
|
|
text*[xcv2::C, g="@{thm ''HOL.refl''}"]\<open>Lorem ipsum ...\<close>
|
|
|
|
|
|
|
|
text\<open>Major sample: test-item of doc-class \verb+F+ with a relational link, and links to formal
|
|
|
|
Isabelle items. \<close>
|
2018-09-17 14:48:05 +00:00
|
|
|
text*[xcv4::F, r="[@{thm ''HOL.refl''},
|
2018-09-11 12:15:11 +00:00
|
|
|
@{thm ''InnerSyntaxAntiquotations.murks''}]",
|
2018-09-17 14:48:05 +00:00
|
|
|
b="{(@{docitem ''xcv1''},@{docitem ''xcv2''})}",
|
2018-09-11 11:51:25 +00:00
|
|
|
s="[@{typ ''int list''}]"]\<open>Lorem ipsum ...\<close>
|
2018-09-11 10:08:25 +00:00
|
|
|
|
2018-09-17 14:48:05 +00:00
|
|
|
text\<open>... and here we add a relation between @{docitem \<open>xcv3\<close>} and @{docitem \<open>xcv2\<close>}
|
2018-09-17 14:58:38 +00:00
|
|
|
into the relation \verb+b+ of @{docitem_ref \<open>xcv4\<close>} \<close>
|
2018-09-17 14:48:05 +00:00
|
|
|
update_instance*[xcv4::F, b+="{(@{docitem ''xcv3''},@{docitem ''xcv2''})}"]
|
|
|
|
|
2018-09-17 14:58:38 +00:00
|
|
|
text\<open>And here is the result on term level:\<close>
|
|
|
|
ML\<open> @{docitem_attr b::xcv4} \<close>
|
2018-09-06 10:07:37 +00:00
|
|
|
|
|
|
|
end
|