Small things at CENELEC arising from FM paper.
HOL-OCL/Isabelle_DOF/master This commit looks good
Details
HOL-OCL/Isabelle_DOF/master This commit looks good
Details
text_elem according to common discussopn with Achim.
This commit is contained in:
parent
3e3fc502c3
commit
436d41d232
10
Isa_COL.thy
10
Isa_COL.thy
|
@ -60,15 +60,13 @@ we follow LaTeX terminology on levels
|
||||||
for scholarly paper: invariant level > 0 \<close>
|
for scholarly paper: invariant level > 0 \<close>
|
||||||
|
|
||||||
doc_class text_element =
|
doc_class text_element =
|
||||||
level :: "int option" <= "None"
|
level :: "int option" <= "None"
|
||||||
(*
|
referentiable :: bool <= "False"
|
||||||
referentiable :: boolean <= "false"
|
variants :: "String.literal set" <= "{STR ''outline'', STR ''document''}"
|
||||||
variants :: "string_literal set" <= "{''outline'', ''document''}"
|
|
||||||
*)
|
|
||||||
|
|
||||||
section\<open>Some attempt to model standardized links to Standard Isabelle Formal Content\<close>
|
section\<open>Some attempt to model standardized links to Standard Isabelle Formal Content\<close>
|
||||||
|
|
||||||
doc_class assertions =
|
doc_class assertions =
|
||||||
properties :: "term list"
|
properties :: "term list"
|
||||||
|
|
||||||
doc_class "thms" =
|
doc_class "thms" =
|
||||||
|
|
|
@ -358,6 +358,7 @@ for exported constraints assuring in judgements safety requirements of the syste
|
||||||
|
|
||||||
doc_class SRAC = EC +
|
doc_class SRAC = EC +
|
||||||
assumption_kind :: ass_kind <= (*default *) formal
|
assumption_kind :: ass_kind <= (*default *) formal
|
||||||
|
formal_repr :: "thm list"
|
||||||
type_synonym safety_related_application_condition = SRAC
|
type_synonym safety_related_application_condition = SRAC
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue