Adding missing files for CENLEC example.

examples/cenelec/mini_odo/ROOT

@@ -0,0 +1,11 @@
+session "mini_odo" = "Isabelle_DOF" +
+  options [document = pdf, document_output = "output"]
+  theories [document = false]
+    (* Foo *)
+    (* Bar *)
+  theories
+    "mini_odo"
+  document_files
+    "isadof.cfg"
+    "preamble.tex"
+    "build"

examples/cenelec/mini_odo/document/build

@@ -0,0 +1,46 @@
+#!/usr/bin/env bash
+# Copyright (c) 2018-2019 The University of Sheffield. All rights reserved.
+#               2018 The University of Paris-Sud. All rights reserved.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions
+# are met:
+# 1. Redistributions of source code must retain the above copyright
+#    notice, this list of conditions and the following disclaimer.
+# 2. Redistributions in binary form must reproduce the above copyright
+#    notice, this list of conditions and the following disclaimer in
+#    the documentation and/or other materials provided with the
+#    distribution.
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
+# FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
+# COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
+# INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
+# BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+# LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+# LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
+# ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+# POSSIBILITY OF SUCH DAMAGE.
+#
+# SPDX-License-Identifier: BSD-2-Clause
+
+set -e
+if [ ! -f $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh ]; then
+    echo ""
+    echo "Error: Isabelle/DOF not installed"
+    echo "====="
+    echo "This is a Isabelle/DOF project. The document preparation requires"
+    echo "the Isabelle/DOF framework. Please obtain the framework by cloning"
+    echo "the Isabelle/DOF git repository, i.e.: "
+    echo "    git clone https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF"
+    echo "You can install the framework as follows:"
+    echo "    cd Isabelle_DOF/document-generator"
+    echo "    ./install"
+    echo ""
+    exit 1
+fi
+
+cp $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh .
+source build_lib.sh

examples/cenelec/mini_odo/document/isadof.cfg

@@ -0,0 +1,3 @@
+Template: scrartcl
+Ontology: scholarly_paper
+Ontology: cenelec_50128

examples/cenelec/mini_odo/document/preamble.tex

@@ -0,0 +1,3 @@
+%% This is a placeholder for user-specific configuration and packages.
+\title{mini-odo}{}{}{}{}{}{}
+\author{By brucker}{}{}{}{}{}

examples/cenelec/mini_odo/mini_odo.thy

@@ -0,0 +1,90 @@
+
+theory mini_odo
+  imports  "Isabelle_DOF.CENELEC_50128" 
+           "Isabelle_DOF.scholarly_paper"
+begin
+
+section\<open> Some examples of Isabelle's standard antiquotations. \<close>
+(* some show-off of standard anti-quotations: *) 
+text \<open>THIS IS A TEXT\<close>
+
+text\<open>  @{thm refl}  of name @{thm [source] refl} 
+        @{thm[mode=Rule] conjI}
+        @{file "mini_odo.thy"} 
+        @{value "3+4::int"} 
+        @{const hd} 
+        @{theory List}
+        @{term "3"} 
+        @{type bool}  
+        @{term [show_types] "f x = a + x"} \<close>
+
+
+
+
+section\<open> Core Examples for stating text-elements as doc-items.\<close>
+
+text\<open>An "anonymous" text-item, automatically coerced into the top-class "text".\<close>
+text*[tralala] \<open> Brexit means Brexit \<close> 
+
+text\<open>Examples for declaration of typed doc-items "assumption" and "hypothesis",
+     concepts defined in the underlying ontology @{theory "CENELEC_50128"}. \<close>
+text*[ass1::assumption] \<open> The subsystem Y is safe. \<close>
+text*[hyp1::hypothesis] \<open> P not equal NP \<close>
+  
+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_50128"}
+     ontology:\<close>  
+
+text*[new_ass::hypothesis]\<open>Under the assumption @{assumption \<open>ass1\<close>} we establish the following: ... \<close>
+
+text*[ass122::srac] \<open> The overall sampling frequence of the odometer
+subsystem is therefore 14 khz, which includes sampling, computing and
+result communication times... \<close>
+  
+text*[t10::test_result] \<open> This is a meta-test. This could be an ML-command
+that governs the external test-execution via, eg., a makefile or specific calls
+to a test-environment or test-engine \<close>
+
+
+section\<open> References to doc-items.\<close>
+text\<open>Finally some examples of references to doc-items, i.e. text-elements with declared 
+     meta-information and status. \<close> 
+text \<open> As established by @{docref (unchecked) \<open>t10\<close>}, 
+                         @{docref (define) \<open>t10\<close>} \<close>
+text \<open> the               @{docref \<open>t10\<close>}                      
+       as well as the    @{docref \<open>ass122\<close>}\<close>  
+text \<open> represent a justification of the safety related applicability 
+       condition @{srac \<open>ass122\<close>} aka exported constraint @{ec \<open>ass122\<close>}.\<close> 
+
+
+
+
+section\<open> Some Tests for Ontology Framework and its CENELEC Instance \<close>  
+                                                  
+declare_reference* [lalala::requirement, alpha="main", beta=42]
+declare_reference* [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1]
+
+
+
+
+
+section*[h::example]\<open> Some global inspection commands for the status of docitem  and doc-class tables ... \<close>  
+
+
+
+section*[i::example]\<open> Text Antiquotation Infrastructure ... \<close>  
+                  
+text\<open> @{docitem \<open>lalala\<close>}   -- produces warning. \<close>  
+text\<open> @{docitem (unchecked) \<open>lalala\<close>} -- produces no warning. \<close>  
+
+text\<open> @{docitem \<open>ass122\<close>} -- global reference to a text-item in another file. \<close>
+
+text\<open> @{ec \<open>ass122\<close>} -- global reference to a exported constraint in another file.
+                         Note that the link is actually a srac, which, according to 
+                         the ontology, happens to be an "ec".  \<close>
+   
+
+  
+end
+  
+