diff --git a/examples/simple/Concept_Example.thy b/examples/simple/Concept_Example.thy deleted file mode 100644 index fadb3bb..0000000 --- a/examples/simple/Concept_Example.thy +++ /dev/null @@ -1,55 +0,0 @@ -chapter\Setting and modifying attributes of doc-items\ - -theory Concept_Example - imports "../../ontologies/Conceptual" (* we use the generic "Conceptual" ontology *) -begin - -text\@{theory \Draft.Conceptual\} provides a monitor @{typ M} enforcing a particular document - structure. Here, we say: From now on, this structural rules are respected wrt. all - \<^theory_text>\doc_class\es @{typ M} is enabled for.\ -open_monitor*[struct::M] - -section*[a::A, x = "3"] \ Lorem ipsum dolor sit amet, ... \ - -text*[c1::C, x = "''beta''"] \ ... suspendisse non arcu malesuada mollis, nibh morbi, ... \ - -text*[d::D, a1 = "X3"] \ ... phasellus amet id massa nunc, pede suscipit repellendus, - ... @{C c1} @{thm "refl"}\ - - -update_instance*[d::D, a1 := X2] - -text\ ... in ut tortor ... @{docitem \a\} ... @{A \a\}\ - -text*[c2::C, x = "''delta''"] \ ... in ut tortor eleifend augue pretium consectetuer. \ - -text*[f::F] \ Lectus accumsan velit ultrices, ... }\ - -theorem some_proof : "P" sorry - -text\This is an example where we add a theorem into a kind of "result-list" of the doc-item f.\ -update_instance*[f::F,r:="[@{thm ''Concept_Example.some_proof''}]"] - -text\ ..., mauris amet, id elit aliquam aptent id, ... @{docitem \a\} \ - -text\Here we add and maintain a link that is actually modeled as m-to-n relation ... - The type annotations with @{typ A} and @{typ C} are optional and may help to get - additional information at the HOL level, the arguments of the inner-syntax antiquotation - are strings that can be denoted in two different syntactic variants; the former is - more robust that the traditional latter.\ -update_instance*[f::F,b:="{(@{docitem \a\}::A,@{docitem \c1\}::C), - (@{docitem ''a''}, @{docitem ''c2''})}"] - -close_monitor*[struct] - -text\And the trace of the monitor is:\ -ML\@{trace_attribute struct}\ - -print_doc_classes -print_doc_items - -check_doc_global - - -end - \ No newline at end of file