forked from Isabelle_DOF/Isabelle_DOF
c0afe1105e
By default invariants checking generates warnings. If invariants_strict_checking theory option is enabled, the checking generates errors. - Update 2018-cicm-isabelle_dof-applications/IsaDofApplications.thy and 2020-iFM-CSP/paper.thy to pass the checking of the low level invariant checking function "check" in scholarly_paper.thy, which checks that the instances in a sequence of the same class have a growing level. For a sequence: section*[intro::introduction]‹ Introduction › text*[introtext::introduction, level = "Some 1"]‹...› introtext must have a level >= than intro. - Bypass the checking of high-level invariants when the class default_cid = "text", the top (default) document class. We want the class default_cid to stay abstract and not have the capability to be defined with attribute, invariants, etc. Hence this bypass handles docitem without a class associated, for example when you just want a document element to be referenceable without using the burden of ontology classes. ex: text*[sdf]\<open> Lorem ipsum @{thm refl}\<close> The functions get_doc_class_global and get_doc_class_local trigger an error when the class is "text" (default_cid), then the functions like check_invariants which use it will fail if the checking is enabled by default for all the theories. |
||
---|---|---|
.. | ||
2018-cicm-isabelle_dof-applications | ||
2020-iFM-CSP | ||
ROOTS |