From ff3f2c9429b65502788fcd644e9603c839ac2158 Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Wed, 13 Mar 2019 12:49:29 +0100
Subject: [PATCH] minor changes for CICM paper example.

---
 Isa_DOF.thy               |  8 +++++---
 ontologies/small_math.thy | 18 +++++++++++++++++-
 2 files changed, 22 insertions(+), 4 deletions(-)

diff --git a/Isa_DOF.thy b/Isa_DOF.thy
index 6a8bac4..7270595 100644
--- a/Isa_DOF.thy
+++ b/Isa_DOF.thy
@@ -1482,9 +1482,11 @@ val _ = Theory.setup((docitem_antiquotation @{binding docref} DOF_core.default_c
                      (* deprecated syntax             ^^^^^^*)
                      (docitem_antiquotation @{binding docitem_ref} DOF_core.default_cid) #>
                      (* deprecated syntax             ^^^^^^^^^^*)
-
-                     (docitem_antiquotation @{binding docitem} DOF_core.default_cid) #>
-                     ML_Antiquotation.inline @{binding docitem_value} ML_antiquotation_docitem_value)
+                     docitem_antiquotation @{binding docitem} DOF_core.default_cid #>
+    (*                 Thy_Output.antiquotation @{binding docitem} docitem_antiquotation_parser 
+                                                                 (docitem_antiquotation_generic DOF_core.default_cid) #>
+     *)
+                ML_Antiquotation.inline  @{binding docitem_value} ML_antiquotation_docitem_value)
 
 end (* struct *)
 \<close>
diff --git a/ontologies/small_math.thy b/ontologies/small_math.thy
index 6a1bb70..437bc18 100644
--- a/ontologies/small_math.thy
+++ b/ontologies/small_math.thy
@@ -47,7 +47,23 @@ datatype kind = expert_opinion | argument | "proof"
 
 doc_class result = technical +
     evidence  :: kind 
-    property  :: "thm list" <= "[]"
+    c  :: "thm list" <= "[]"
+
+
+
+ML\<open>fun check_invariant_invariant oid {is_monitor:bool} ctxt =
+      let val kind_term = AttributeAccess.compute_attr_access ctxt "kind" oid @{here} @{here} 
+          val property_termS = AttributeAccess.compute_attr_access ctxt "property" oid @{here} @{here} 
+          val tS = HOLogic.dest_list property_termS
+      in  case kind_term of
+            @{term "proof"} => if not(null tS) then true
+                               else error("class class invariant violation") 
+           | _ => false
+      end
+\<close>
+
+setup\<open>DOF_core.update_class_invariant "small_math.result" check_invariant_invariant\<close>
+
 
 doc_class example    = technical +
     referring_to :: "(notion + definition) set" <=  "{}"