merge commit

Isa_DOF.thy

@@ -35,7 +35,7 @@ consts mk_docitem :: "string \<Rightarrow> 'a"      ("@{docitem _}")
 term "@{typ  ''int => int''}"  
 term "@{term ''Bound 0''}"  
 term "@{thm  ''refl''}"  
-term "@{thm  ''<doc_ref>''}"
+term "@{docitem  ''<doc_ref>''}"
   
   
   

examples/simple/Concept_Example.thy

@@ -4,14 +4,33 @@ begin
 
 open_monitor*[struct::M]  
 
-section*[a::A, x = "''alpha''"] \<open> AAA \<close>
+section*[a::A, x = "''alpha''"] \<open> Lorem ipsum dolor sit amet, ... \<close>
 
+text*[c1::C, x = "''beta''"] 
+\<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ...  \<close>
+  
+text*[d::D, a1 = "X3"] 
+\<open> ... phasellus amet id massa nunc, pede suscipit repellendus, ... \<close>
 
-text*[c1::C, x = "''beta''"] \<open> C \<close>
-text*[d ::D, x = "''gamma''"] \<open> D \<close>
-text*[c2 ::C, x = "''delta''"] \<open> C \<close>
+update_instance*[d::D, a1 := X2]
 
-section*[f::F]  \<open> D \<close>
+text{* ... in ut tortor ... @{docitem_ref \<open>a\<close>} ... @{A \<open>a\<close>}*}  
+  
+(* text{* ... in ut tortor ... @{docitem_ref \<open>a\<close>} ... @{C \<open>a\<close>}*}  *)
+  
+text*[c2::C, x = "''delta''"] 
+\<open> ... in ut tortor eleifend augue pretium consectetuer.  \<close>
+
+section*[f::F] \<open> Lectus accumsan velit ultrices, ... }\<close>
+  
+theorem some_proof : "P" sorry
+    
+update_instance*[f,r:="[@{thm ''some_proof''}]"]
+
+text{* ..., mauris amet, id elit aliquam aptent id,  ... *}
+  
+update_instance*[f,b:="{(@{docitem  ''a''}::A,@{docitem  ''c1''}::C), 
+                        (@{docitem  ''a''},@{docitem  ''c1''})}"] 
   
 close_monitor*[struct]
 

ontologies/Conceptual.thy

@@ -19,7 +19,7 @@ doc_class D = B +
 
 doc_class F  = 
    r :: "thm list"
-   b :: "(A \<times> B) set"   <= "{}"
+   b :: "(A \<times> C) set"   <= "{}"
 
 doc_class M = 
    trace :: "(A + C + D + F) list"