diff --git a/Isa_COL.thy b/Isa_COL.thy index 4d02616..db3f53a 100644 --- a/Isa_COL.thy +++ b/Isa_COL.thy @@ -60,15 +60,13 @@ we follow LaTeX terminology on levels for scholarly paper: invariant level > 0 \ doc_class text_element = - level :: "int option" <= "None" -(* - referentiable :: boolean <= "false" - variants :: "string_literal set" <= "{''outline'', ''document''}" -*) + level :: "int option" <= "None" + referentiable :: bool <= "False" + variants :: "String.literal set" <= "{STR ''outline'', STR ''document''}" section\Some attempt to model standardized links to Standard Isabelle Formal Content\ -doc_class assertions = +doc_class assertions = properties :: "term list" doc_class "thms" = diff --git a/ontologies/CENELEC_50128.thy b/ontologies/CENELEC_50128.thy index eed6a0d..29e7692 100644 --- a/ontologies/CENELEC_50128.thy +++ b/ontologies/CENELEC_50128.thy @@ -358,6 +358,7 @@ for exported constraints assuring in judgements safety requirements of the syste doc_class SRAC = EC + assumption_kind :: ass_kind <= (*default *) formal + formal_repr :: "thm list" type_synonym safety_related_application_condition = SRAC