Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Renamed CENELEC_50126 to CENELEC_50128 to match actual standard.

This commit is contained in:
Achim D. Brucker 2019-02-05 09:42:12 +00:00
parent 0a35d3029e
commit bebf83673a
7 changed files with 15 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
README.md
View File

@ -96,7 +96,7 @@ Usage: isabelle DOF_mkroot [OPTIONS] [DIR]
-n NAME alternative session name (default: DIR base name) -n NAME alternative session name (default: DIR base name)
-o ONTOLOGY (default: core) -o ONTOLOGY (default: core)
Available ontologies: Available ontologies:
* cenelec_50126 * cenelec_50128
* core * core
* mathex * mathex
* scholarly_paper * scholarly_paper

2
ROOT
View File

@ -4,7 +4,7 @@ session "Isabelle_DOF" = "Functional-Automata" +
"Regular-Sets" "Regular-Sets"
theories theories
Isa_DOF Isa_DOF
"ontologies/CENELEC_50126" "ontologies/CENELEC_50128"
"ontologies/Conceptual" "ontologies/Conceptual"
"ontologies/scholarly_paper" "ontologies/scholarly_paper"
"ontologies/technical_report" "ontologies/technical_report"

4
document-generator/latex/DOF-cenelec_50126.sty → document-generator/latex/DOF-cenelec_50128.sty
View File

@ -12,9 +12,9 @@
%% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause %% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause
\NeedsTeXFormat{LaTeX2e}\relax \NeedsTeXFormat{LaTeX2e}\relax
\ProvidesPackage{DOF-cenelec_50126} \ProvidesPackage{DOF-cenelec_50128}
[0000/00/00 Unreleased v0.0.0+% [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} \RequirePackage{DOF-core}

6
examples/cenelec/Example.thy
View File

@ -1,7 +1,7 @@
chapter\<open> Example : Forward and Standard (use-after-define) Referencing\<close> chapter\<open> Example : Forward and Standard (use-after-define) Referencing\<close>
theory Example theory Example
imports "../../ontologies/CENELEC_50126" imports "../../ontologies/CENELEC_50128"
"../../ontologies/scholarly_paper" "../../ontologies/scholarly_paper"
begin begin
@ -28,12 +28,12 @@ text\<open>An "anonymous" text-item, automatically coerced into the top-class "t
text*[tralala] \<open> Brexit means Brexit \<close> text*[tralala] \<open> Brexit means Brexit \<close>
text\<open>Examples for declaration of typed doc-items "assumption" and "hypothesis", text\<open>Examples for declaration of typed doc-items "assumption" and "hypothesis",
concepts defined in the underlying ontology @{theory "CENELEC_50126"}. \<close> concepts defined in the underlying ontology @{theory "CENELEC_50128"}. \<close>
text*[ass1::assumption] \<open> The subsystem Y is safe. \<close> text*[ass1::assumption] \<open> The subsystem Y is safe. \<close>
text*[hyp1::hypothesis] \<open> P inequal NP \<close> text*[hyp1::hypothesis] \<open> P inequal NP \<close>
text\<open>A real example fragment from a larger project, declaring a text-element as a text\<open>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:\<close> ontology:\<close>
text*[new_ass::hypothesis]\<open>Under the assumption @{assumption \<open>ass1\<close>} we establish the following: ... \<close> text*[new_ass::hypothesis]\<open>Under the assumption @{assumption \<open>ass1\<close>} we establish the following: ... \<close>

12
ontologies/CENELEC_50126.thy → ontologies/CENELEC_50128.thy
View File

@ -11,7 +11,7 @@ identifies:
\<close> \<close>
(*<<*) (*<<*)
theory CENELEC_50126 theory CENELEC_50128
imports "../Isa_COL" imports "../Isa_COL"
begin begin
(*>>*) (*>>*)
@ -311,7 +311,7 @@ text\<open>The category @{emph \<open>hypothesis\<close>} is used for assumption
datatype hyp_type = physical | mathematical | computational | other datatype hyp_type = physical | mathematical | computational | other
typ "CENELEC_50126.requirement" typ "CENELEC_50128.requirement"
doc_class hypothesis = requirement + doc_class hypothesis = requirement +
hyp_type :: hyp_type <= physical (* default *) 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 "srac" @{theory};
DOF_core.is_defined_cid_global "ec" @{theory}; DOF_core.is_defined_cid_global "ec" @{theory};
"XXXXXXXXXXXXXXXXX"; "XXXXXXXXXXXXXXXXX";
DOF_core.is_subclass @{context} "CENELEC_50126.ec" "CENELEC_50126.ec"; DOF_core.is_subclass @{context} "CENELEC_50128.ec" "CENELEC_50128.ec";
DOF_core.is_subclass @{context} "CENELEC_50126.srac" "CENELEC_50126.ec"; DOF_core.is_subclass @{context} "CENELEC_50128.srac" "CENELEC_50128.ec";
DOF_core.is_subclass @{context} "CENELEC_50126.ec" "CENELEC_50126.srac"; DOF_core.is_subclass @{context} "CENELEC_50128.ec" "CENELEC_50128.srac";
DOF_core.is_subclass @{context} "CENELEC_50126.ec" "CENELEC_50126.test_requirement"; DOF_core.is_subclass @{context} "CENELEC_50128.ec" "CENELEC_50128.test_requirement";
"XXXXXXXXXXXXXXXXX"; "XXXXXXXXXXXXXXXXX";
val {docobj_tab={maxano, tab=ref_tab},docclass_tab=class_tab,...} = DOF_core.get_data @{context}; val {docobj_tab={maxano, tab=ref_tab},docclass_tab=class_tab,...} = DOF_core.get_data @{context};
Symtab.dest ref_tab; Symtab.dest ref_tab;

2
test/cenelec/Example.thy
View File

@ -1,5 +1,5 @@
theory Example theory Example
imports "../../ontologies/CENELEC_50126" imports "../../ontologies/CENELEC_50128"
begin begin
section{* Some show-off's of general antiquotations. *} section{* Some show-off's of general antiquotations. *}

2
test/simple/Example.thy
View File

@ -1,5 +1,5 @@
theory Example theory Example
imports "../../ontologies/CENELEC_50126" imports "../../ontologies/CENELEC_50128"
keywords "Term" :: diag keywords "Term" :: diag
begin begin