From 4f349de9b9b3405b66f7ff1204755fe5ee56544d Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Sat, 6 Apr 2019 12:08:38 +0200
Subject: [PATCH] some patches in install to make it run on MacOS

---
 examples/cenelec/Example.thy     | 92 ++++++++++++++++++++++++++++++++
 examples/math_exam/Noodles.thy   |  5 ++
 examples/math_exam/On_Noodle.thy | 30 +++++++++++
 3 files changed, 127 insertions(+)
 create mode 100644 examples/cenelec/Example.thy
 create mode 100644 examples/math_exam/Noodles.thy
 create mode 100644 examples/math_exam/On_Noodle.thy

diff --git a/examples/cenelec/Example.thy b/examples/cenelec/Example.thy
new file mode 100644
index 0000000..803c5ee
--- /dev/null
+++ b/examples/cenelec/Example.thy
@@ -0,0 +1,92 @@
+chapter\<open> Example : Forward and Standard (use-after-define) Referencing\<close>
+
+theory Example
+  imports  "../../ontologies/CENELEC_50128" 
+           "../../ontologies/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 "../../Isa_DOF.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]
+
+paragraph* [sdfk::introduction] \<open> just a paragraph - lexical variant \<close>
+
+
+
+
+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
+  
+    
\ No newline at end of file
diff --git a/examples/math_exam/Noodles.thy b/examples/math_exam/Noodles.thy
new file mode 100644
index 0000000..5a9be9e
--- /dev/null
+++ b/examples/math_exam/Noodles.thy
@@ -0,0 +1,5 @@
+theory Noodles
+  imports "small_math"
+begin
+
+title*[t::title]\<open>On Noodles\<close>
\ No newline at end of file
diff --git a/examples/math_exam/On_Noodle.thy b/examples/math_exam/On_Noodle.thy
new file mode 100644
index 0000000..91aa424
--- /dev/null
+++ b/examples/math_exam/On_Noodle.thy
@@ -0,0 +1,30 @@
+theory "On_Noodle"
+  imports small_math
+begin
+
+open_monitor*[this::article]
+
+title*[t1::title]\<open>On Noodles\<close> 
+
+text*[simon::author]\<open>Simon Foster\<close>
+text*[a::abstract, keyword_list = "[topology]"]
+\<open>We present the first fundamental results on the goundbreaking theory of noodles...\<close>
+section*[intro::introduction]\<open>Introduction\<close>
+
+text\<open> Authorities say, that Noodles are unleavened dough which is stretched,
+ extruded, or rolled flat and cut into one or a variety of shapes which usually 
+include long, thin strips, or waves, helices, tubes, strings, or shells, or 
+folded over, or cut into other shapes. Noodles are usually cooked in boiling water, 
+sometimes with cooking oil or salt added. \<close>
+
+section*[def_sec::technical]\<open>Basic definitions\<close>
+
+text*[d1::"definition"]\<open>My first definition\<close>
+definition noodle ::"bool" where "noodle = (THE x. True)" 
+
+(*
+update_instance*[def1, formal_results:="[@{thm ''noodle_def''}]"]
+*)
+
+close_monitor*[this::article]
+