diff --git a/README.md b/README.md index b0a8192..b2544f6 100644 --- a/README.md +++ b/README.md @@ -96,7 +96,7 @@ Usage: isabelle DOF_mkroot [OPTIONS] [DIR] -n NAME alternative session name (default: DIR base name) -o ONTOLOGY (default: core) Available ontologies: - * cenelec_50126 + * cenelec_50128 * core * mathex * scholarly_paper diff --git a/ROOT b/ROOT index 7254537..a975506 100644 --- a/ROOT +++ b/ROOT @@ -4,7 +4,7 @@ session "Isabelle_DOF" = "Functional-Automata" + "Regular-Sets" theories Isa_DOF - "ontologies/CENELEC_50126" + "ontologies/CENELEC_50128" "ontologies/Conceptual" "ontologies/scholarly_paper" "ontologies/technical_report" diff --git a/document-generator/latex/DOF-cenelec_50126.sty b/document-generator/latex/DOF-cenelec_50128.sty similarity index 92% rename from document-generator/latex/DOF-cenelec_50126.sty rename to document-generator/latex/DOF-cenelec_50128.sty index 9038f26..6971d7d 100644 --- a/document-generator/latex/DOF-cenelec_50126.sty +++ b/document-generator/latex/DOF-cenelec_50128.sty @@ -12,9 +12,9 @@ %% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause \NeedsTeXFormat{LaTeX2e}\relax -\ProvidesPackage{DOF-cenelec_50126} +\ProvidesPackage{DOF-cenelec_50128} [0000/00/00 Unreleased v0.0.0+% - Document-Type Support Framework for Isabelle (CENELEC 50126).] + Document-Type Support Framework for Isabelle (CENELEC 50128).] \RequirePackage{DOF-core} diff --git a/examples/cenelec/Example.thy b/examples/cenelec/Example.thy index 02694d9..7fd66bb 100644 --- a/examples/cenelec/Example.thy +++ b/examples/cenelec/Example.thy @@ -1,7 +1,7 @@ chapter\ Example : Forward and Standard (use-after-define) Referencing\ theory Example - imports "../../ontologies/CENELEC_50126" + imports "../../ontologies/CENELEC_50128" "../../ontologies/scholarly_paper" begin @@ -28,12 +28,12 @@ text\An "anonymous" text-item, automatically coerced into the top-class "t text*[tralala] \ Brexit means Brexit \ text\Examples for declaration of typed doc-items "assumption" and "hypothesis", - concepts defined in the underlying ontology @{theory "CENELEC_50126"}. \ + concepts defined in the underlying ontology @{theory "CENELEC_50128"}. \ text*[ass1::assumption] \ The subsystem Y is safe. \ text*[hyp1::hypothesis] \ P inequal NP \ text\A real example fragment from a larger project, declaring a text-element as a - "safety-related application condition", a concept defined in the @{theory "CENELEC_50126"} + "safety-related application condition", a concept defined in the @{theory "CENELEC_50128"} ontology:\ text*[new_ass::hypothesis]\Under the assumption @{assumption \ass1\} we establish the following: ... \ diff --git a/ontologies/CENELEC_50126.thy b/ontologies/CENELEC_50128.thy similarity index 98% rename from ontologies/CENELEC_50126.thy rename to ontologies/CENELEC_50128.thy index bf52f91..358e9b3 100644 --- a/ontologies/CENELEC_50126.thy +++ b/ontologies/CENELEC_50128.thy @@ -11,7 +11,7 @@ identifies: \ (*<<*) -theory CENELEC_50126 +theory CENELEC_50128 imports "../Isa_COL" begin (*>>*) @@ -311,7 +311,7 @@ text\The category @{emph \hypothesis\} is used for assumption datatype hyp_type = physical | mathematical | computational | other -typ "CENELEC_50126.requirement" +typ "CENELEC_50128.requirement" doc_class hypothesis = requirement + hyp_type :: hyp_type <= physical (* default *) @@ -426,10 +426,10 @@ DOF_core.name2doc_class_name @{theory} "srac"; DOF_core.is_defined_cid_global "srac" @{theory}; DOF_core.is_defined_cid_global "ec" @{theory}; "XXXXXXXXXXXXXXXXX"; -DOF_core.is_subclass @{context} "CENELEC_50126.ec" "CENELEC_50126.ec"; -DOF_core.is_subclass @{context} "CENELEC_50126.srac" "CENELEC_50126.ec"; -DOF_core.is_subclass @{context} "CENELEC_50126.ec" "CENELEC_50126.srac"; -DOF_core.is_subclass @{context} "CENELEC_50126.ec" "CENELEC_50126.test_requirement"; +DOF_core.is_subclass @{context} "CENELEC_50128.ec" "CENELEC_50128.ec"; +DOF_core.is_subclass @{context} "CENELEC_50128.srac" "CENELEC_50128.ec"; +DOF_core.is_subclass @{context} "CENELEC_50128.ec" "CENELEC_50128.srac"; +DOF_core.is_subclass @{context} "CENELEC_50128.ec" "CENELEC_50128.test_requirement"; "XXXXXXXXXXXXXXXXX"; val {docobj_tab={maxano, tab=ref_tab},docclass_tab=class_tab,...} = DOF_core.get_data @{context}; Symtab.dest ref_tab; diff --git a/test/cenelec/Example.thy b/test/cenelec/Example.thy index 48756f8..cd5c874 100644 --- a/test/cenelec/Example.thy +++ b/test/cenelec/Example.thy @@ -1,5 +1,5 @@ theory Example - imports "../../ontologies/CENELEC_50126" + imports "../../ontologies/CENELEC_50128" begin section{* Some show-off's of general antiquotations. *} diff --git a/test/simple/Example.thy b/test/simple/Example.thy index 47106ee..718869a 100644 --- a/test/simple/Example.thy +++ b/test/simple/Example.thy @@ -1,5 +1,5 @@ theory Example - imports "../../ontologies/CENELEC_50126" + imports "../../ontologies/CENELEC_50128" keywords "Term" :: diag begin