Common developments on

- library
- presentation attribute
- factorisation of Common Ontology Library (COL)
- new infrastructure report

Isa_COL.thy

@@ -0,0 +1,41 @@
+chapter \<open>The Document Ontology Common Library for the Isabelle Ontology Framework\<close>
+
+text\<open> Offering 
+\<^item> ...
+\<^item> 
+\<^item> LaTeX support. \<close> 
+  
+  
+theory Isa_COL   
+  imports  Isa_DOF  
+begin
+  
+   
+section\<open> Library of Standard Text Ontology \<close>
+
+datatype placement = pl_h | pl_t | pl_b | pl_ht | pl_hb   
+doc_class figure   = 
+   relative_width   :: "int" (* percent of textwidth *)    
+   src              :: "string"
+   placement        :: placement 
+   spawn_columns    :: bool <= True 
+
+doc_class side_by_side_figure = figure +
+   anchor           :: "string"
+   caption          :: "string"
+   relative_width2  :: "int" (* percent of textwidth *)    
+   src2             :: "string"
+   anchor2          :: "string"
+   caption2         :: "string"
+
+doc_class figure_group = 
+ (*  trace            :: "doc_class rexp list" <= "[]" *)
+   anchor           :: "string"
+   caption          :: "string"
+   where "\<lbrace>figure\<rbrace>\<^sup>+"
+
+(* dito the future table *)
+
+(* dito the future monitor: table - block *)
+
+end

Isa_DOF.thy

@@ -1393,35 +1393,6 @@ val _ =
 end (* struct *)
 \<close>  
 
-  
-   
-section\<open> Library of Standard Text Ontology \<close>
-
-datatype placement = pl_h | pl_t | pl_b | pl_ht | pl_hb   
-doc_class figure   = 
-   relative_width   :: "int" (* percent of textwidth *)    
-   src              :: "string"
-   placement        :: placement 
-   spawn_columns    :: bool <= True 
-
-doc_class side_by_side_figure = figure +
-   anchor           :: "string"
-   caption          :: "string"
-   relative_width2  :: "int" (* percent of textwidth *)    
-   src2             :: "string"
-   anchor2          :: "string"
-   caption2         :: "string"
-
-doc_class figure_group = 
- (*  trace            :: "doc_class rexp list" <= "[]" *)
-   anchor           :: "string"
-   caption          :: "string"
-   where "\<lbrace>figure\<rbrace>\<^sup>+"
-
-(* dito the future table *)
-
-(* dito the future monitor: table - block *)
-
 section\<open> Testing and Validation \<close>
   
 text*[sdf] {* f @{thm refl}*}  
@@ -1444,5 +1415,4 @@ ML\<open> fold_aterms  Term.add_free_names;
     fold_aterms  Term.add_var_names;\<close>
 
 
-
 end

ontologies/scholarly_paper.thy

@@ -1,7 +1,7 @@
 section{* An example ontology for a scholarly paper*}
 
 theory scholarly_paper
-   imports "../Isa_DOF"
+   imports "../Isa_COL"
 begin
 
 doc_class title =

ontologies/technical_report.thy

@@ -0,0 +1,27 @@
+section{* An example ontology for a scholarly paper*}
+
+theory technical_report
+   imports "scholarly_paper"
+begin
+
+doc_class table_of_content =
+   level       :: int <= 3
+
+doc_class "chapter" = text_section +
+   style :: string 
+  
+doc_class report = 
+   style_id :: string                <= "''LNCS''"
+   version  :: "(int \<times> int \<times> int)"  <= "(0,0,0)"
+   where "(title       ~~ 
+           \<lbrakk>subtitle\<rbrakk>   ~~
+           \<lbrace>author\<rbrace>\<^sup>+   ~~ 
+           abstract     ~~
+           chapter      ~~
+           introduction ~~ 
+           \<lbrace>technical || example\<rbrace>\<^sup>+ ~~ 
+           conclusion   ~~  
+           bibliography)"
+
+end
+