Minor corrections on CENELEC,

major Bug in assert* (no assert object creation on-the-fly) fixed

Isa_DOF.thy

@@ -401,17 +401,17 @@ fun declare_anoobject_local ctxt cid =
     end
 
 
-fun get_object_global oid thy  = let val {tab,...} = #docobj_tab(get_data_global thy)
-                                 in  case Symtab.lookup tab oid of 
-                                       NONE => error("undefined reference: "^oid)
-                                      |SOME(bbb) => bbb
-                                 end
+fun get_object_global_opt oid thy  = Symtab.lookup (#tab(#docobj_tab(get_data_global thy))) oid 
 
-fun get_object_local oid ctxt  = let val {tab,...} = #docobj_tab(get_data ctxt)
-                                 in  case Symtab.lookup tab oid of 
+fun get_object_global oid thy  = case get_object_global_opt oid thy of 
+                                       NONE => error("undefined reference: "^oid)
+                                      |SOME(bbb) => bbb
+
+fun get_object_local_opt oid ctxt  = Symtab.lookup (#tab(#docobj_tab(get_data ctxt))) oid
+
+fun get_object_local oid ctxt  = case get_object_local_opt oid ctxt of 
                                        NONE => error("undefined reference: "^oid)
                                       |SOME(bbb) => bbb
-                                 end
 
 fun get_doc_class_global cid thy = 
     if cid = default_cid then error("default doc class acces") (* TODO *)
@@ -1280,8 +1280,9 @@ fun assert_cmd'((((((oid,pos),cid_pos),doc_attrs),some_name:string option),modes
         fun conv_attrs thy = (("property",pos),"[@{term ''"^markup2string prop ^"''}]")::doc_attrs  
         (* fun conv_attrs thy = (("property",pos),"[@{term ''"^parse_convert thy ^"''}]")::doc_attrs *)
         fun conv_attrs' thy = map (fn ((lhs,pos),rhs) => (((lhs,pos),"+="),rhs)) (conv_attrs thy)
-        fun mks thy = case DOF_core.get_object_global oid thy of
-                   SOME _ => (writeln "SOME"; update_instance_command (((oid,pos),cid_pos),conv_attrs' thy) thy)
+        fun mks thy = case DOF_core.get_object_global_opt oid thy of
+                   SOME NONE => (error("update of declared but not created doc_item:" ^ oid))
+                 | SOME _ => (writeln "SOME"; update_instance_command (((oid,pos),cid_pos),conv_attrs' thy) thy)
                  | NONE   => (writeln "NONE"; create_and_check_docitem false oid pos cid_pos (conv_attrs thy) thy)
         val check = (assert_cmd some_name modes prop) o Proof_Context.init_global
     in 

examples/conceptual/AssnsLemmaThmEtc.thy

@@ -27,7 +27,7 @@ text\<open>An example for the ontology specification character of the short-cuts
 different class. "F" and "assertion" have only in common that they posses the attribute
 \<^verbatim>\<open>property\<close>: \<close>
 
-text*[aaa::assertion]\<open>Our definition of the integers has the following properties:\<close>
+text\<open>Creation just like that: \<close>
 assert*[aaa::assertion] "3 < (4::int)"
 assert*[aaa::assertion] "0 < (4::int)"
 

ontologies/CENELEC_50128.thy

@@ -239,7 +239,7 @@ datatype role =  PM  (* Program Manager *)
               |  DES (* Designer *)
               |  IMP (* Implementer *)
               |  ASR (* Assessor *)
-              |  Ne  (* Integrator *)
+              |  INT  (* Integrator *)
               |  TST (* Tester *)
               |  VER (* Verifier *)
               |  VnV (* Verification and Validation *)
@@ -425,11 +425,9 @@ text\<open>The objective of software verification is to examine and arrive at a
 development phase fulfil the requirements and plans with respect to completeness, correctness 
 and consistency. \<close>
 doc_class judgement = 
-   evidence        :: "verification_and_testing_technique list"
+   evidence        :: "vnt_technique list"
    is_concerned    :: "role set" <= "{VER,ASR,VAL}" 
 
-
-
 section\<open> Design and Test Documents \<close> 
 
 doc_class cenelec_text = text_element +