From 436d41d2325c879fdceda6c4a4274deafa4cd93b Mon Sep 17 00:00:00 2001 From: bu Date: Tue, 16 Apr 2019 11:06:21 +0200 Subject: [PATCH] Small things at CENELEC arising from FM paper. text_elem according to common discussopn with Achim. --- Isa_COL.thy | 10 ++++------ ontologies/CENELEC_50128.thy | 1 + 2 files changed, 5 insertions(+), 6 deletions(-) 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