diff --git a/examples/simple/Example.thy b/examples/simple/Example.thy
index 31fcba2..5818c45 100644
--- a/examples/simple/Example.thy
+++ b/examples/simple/Example.thy
@@ -1,5 +1,5 @@
 theory Example
-  imports  "../../CENELEC_50126"
+  imports  "../../ontologies/CENELEC_50126"
   keywords "Term" :: diag 
 begin
 
diff --git a/ontologies/CC_ISO15408.thy b/ontologies/CC_ISO15408.thy
new file mode 100644
index 0000000..e69de29
diff --git a/ontologies/CENELEC_50126.thy b/ontologies/CENELEC_50126.thy
new file mode 100644
index 0000000..d4df3d5
--- /dev/null
+++ b/ontologies/CENELEC_50126.thy
@@ -0,0 +1,216 @@
+chapter \<open>An Outline of a CENELEC Ontology\<close>
+
+text{* NOTE: An Ontology-Model of a certification standard such as CENELEC or
+Common Criteria identifies:
+- notions (conceptual \emph{categories}) having \emph{instances}
+  (similar to classes and objects),
+- their subtype relation (eg., a "SRAC" is an "assumption"),
+- their syntactical structure 
+  (for the moment: defined by regular expressions describing the
+   order of category instances in the overall document as a regular language)
+ *}  
+  
+theory CENELEC_50126
+  imports "../Isa_DOF"
+begin
+
+text{* Excerpt of the BE EN 50128:2011 *}
+
+section {* Requirements-Analysis related Categories *}  
+
+doc_class requirement =
+   long_name :: "string option"
+  
+
+doc_class requirement_analysis = 
+   no :: "nat"
+   where "requirement_item +"
+
+                              
+text{*The category @{emph \<open>hypothesis\<close>} is used for assumptions from the 
+      foundational mathematical or physical domain, so for example: 
+      \<^item>   the Mordell-Lang conjecture holds,   
+      \<^item>   euklidian geometry is assumed, or
+      \<^item>   Newtonian (non-relativistic) physics is assumed,
+      \<^item>   @{term "P \<noteq> NP"},
+      \<^item>   or the computational hardness  of certain functions 
+          relevant for cryptography (like prime-factorization).
+     Their acceptance is inherently outside the scope of the model
+     and can only established inside certification process by
+     authority argument.
+*}
+  
+datatype hyp_type = physical | mathematical | computational | other
+
+
+typ "CENELEC_50126.requirement"
+
+
+doc_class hypothesis = requirement +
+      hyp_type :: hyp_type <= physical  (* default *)
+  
+text{*The category @{emph \<open>assumption\<close>} is used for domain-specific assumptions. 
+      It has formal, semi-formal and informal sub-categories. They have to be 
+      tracked and discharged by appropriate validation procedures within a 
+      certification process, by it by test or proof. *}
+
+datatype ass_kind = informal | semiformal | formal
+  
+doc_class assumption = requirement +
+     assumption_kind :: ass_kind <= informal 
+
+text{*The category @{emph \<open>exported constraint\<close>} (or @{emph \<open>ec\<close>} for short) 
+      is used for formal assumptions, that arise during the analysis,
+      design or implementation and have to be tracked till the final
+      evaluation target,and discharged by appropriate validation procedures 
+      within the certification process, by it by test or proof. *}
+
+doc_class ec = assumption  +
+     assumption_kind :: ass_kind <= (*default *) formal
+
+text{*The category @{emph \<open>safety related application condition\<close>} (or @{emph \<open>srac\<close>} 
+      for short) is used for @{typ ec}'s that establish safety properties
+      of the evaluation target. Their track-ability throughout the certification
+      is therefore particularly critical. *}
+                        
+doc_class srac = ec  +
+     assumption_kind :: ass_kind <= (*default *) formal
+
+section {* Design related Categories *}  
+
+doc_class design_item = 
+      description :: string
+
+datatype design_kind = unit | module | protocol
+      
+doc_class interface =  design_item +
+      kind :: design_kind
+      
+
+section {* Requirements-Analysis related Categories *}  
+
+doc_class test_item =
+      nn :: "string option"
+
+text{* subcategories are : *}
+  
+datatype test_kind = blackbox | whitebox | greybox | fuzz | pertubation
+  
+datatype test_coverage_criterion =  
+             allpathk  nat nat     (* depth, test_coverage_degree *)
+             | mcdc  nat           (* depth, test_coverage_degree *)
+             | exhaustive
+             | dnf_E_d  string nat (* equivalence class testing *)
+             | other string
+    
+doc_class test_specification = test_item +
+          short_goal :: string
+      
+doc_class test_case = test_item +
+          kind  :: test_kind
+          descr :: string
+
+          
+          
+doc_class test_result = test_item +
+             verdict :: bool
+             remarks :: string
+             covvrit :: test_coverage_criterion
+
+datatype   test_environment_kind = hardware_in_the_loop ("hil") 
+                                 | simulated_hardware_in_the_loop ("shil") 
+  
+doc_class  test_environment = test_item +
+             descr :: string
+             kind  :: test_environment_kind <= shil
+
+doc_class  test_tool = test_item +
+             descr :: string
+
+doc_class  test_requirement = test_item +
+             descr :: string
+
+doc_class  test_adm_role = test_item +
+             name :: string
+
+doc_class test_documentation = 
+   no :: "nat"
+   where "(test_specification.((test_case.test_result)+.(test_environment|test_tool))+.
+          [test_requirement].test_adm_role"
+   where "(test_specification.((test_case.test_result)+.(test_environment|test_tool))+.
+          [test_requirement].test_adm_role"
+
+
+
+
+
+
+section{* Example *}
+
+text*[ass122::srac] {* The overall sampling frequence of the odometer
+subsystem is therefore 14 khz, which includes sampling, computing and
+result communication times... *}
+  
+text*[t10::test_result] {* 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 *}
+
+
+text \<open> As established by @{docref \<open>t10\<close>}, the 
+       assumption @{docref \<open>ass122\<close>} is validated. \<close>
+
+                               
+section{* Provisory Setup *}
+
+(* Hack: This should be generated automatically: *)
+ML{*
+val _ = Theory.setup
+        ((DocAttrParser.control_antiquotation @{binding srac}     
+                                              (DOF_core.name2doc_class_name @{theory} "srac")
+                                              {strict_checking=true}  
+                                              "\\autoref{" "}" ) #>
+         (DocAttrParser.control_antiquotation @{binding ec}
+                                              (DOF_core.name2doc_class_name @{theory} "ec")
+                                              {strict_checking=true} 
+                                              "\\autoref{" "}")#>
+         (DocAttrParser.control_antiquotation @{binding test_specification}
+                                              (DOF_core.name2doc_class_name @{theory} "test_specification")
+                                              {strict_checking=true}   
+                                              "\\label{" "}"))
+
+*}
+
+
+
+
+section{* Testing and Validation *}
+
+
+ML{*
+DOF_core.name2doc_class_name @{theory} "requirement";
+DOF_core.name2doc_class_name @{theory} "srac";
+DOF_core.is_defined_cid_global "srac" @{theory};
+DOF_core.is_defined_cid_global "ec" @{theory};
+
+DOF_core.is_subclass @{context} "CENELEC_50126.srac" "CENELEC_50126.ec";
+DOF_core.is_subclass @{context} "CENELEC_50126.ec"   "CENELEC_50126.srac";
+
+val ({maxano, tab},tab2) = DOF_core.get_data @{context};
+Symtab.dest tab;
+Symtab.dest tab2;
+
+
+*}  
+
+
+ML{*
+DOF_core.name2doc_class_name @{theory} "requirement";
+Syntax.parse_typ @{context} "requirement";
+val Type(t,_) = Syntax.parse_typ @{context} "requirement" handle ERROR _ => dummyT;
+Syntax.read_typ  @{context} "hypothesis" handle  _ => dummyT;
+Proof_Context.init_global;
+*}
+
+
+end      
+  
\ No newline at end of file
diff --git a/ontologies/LNCS_onto.thy b/ontologies/LNCS_onto.thy
new file mode 100644
index 0000000..bdff762
--- /dev/null
+++ b/ontologies/LNCS_onto.thy
@@ -0,0 +1,92 @@
+theory LNCS_onto
+  imports Isa_DOF
+begin
+
+doc_class title =
+   short_title :: "string option" -- None
+  
+doc_class subtitle =
+   abbrev :: "string option"      -- None
+
+doc_class author =
+   affiliation :: "string"
+
+doc_class abstract =
+   keywds :: "string list"        -- None
+
+doc_class introduction =
+   main_author :: "author option" -- None
+
+doc_class tech_section =
+   main_author :: "author option" -- None
+
+doc_class example_section =
+   main_author :: "author option" -- None
+
+
+doc_class conclusion =
+   main_author :: "author option" -- None
+
+doc_class bibliography =
+   style :: "string option" -- "''LNCS''"
+
+text{* Besides subtyping, there is another relation between
+       doc_classes: a class can be a \emph{monitor} to other ones,
+       which is expressed by occurrence in the where clause.
+       While sub-classing refers to data-inheritance of attributes,
+       a monitor captures structural constraints -- the order --
+       in which instances of monitored classes may occur.
+
+       The control of monitors is done by the commands:
+       -- monitor <doc-class>
+       -- close_monitor <doc-class> 
+       where the automaton of the monitor class is expected
+       to be in a final state.
+
+       Monitors can be nested.
+ 
+       Classes neither directly or via inheritance indirectly
+       mentioned in the monitor are \emph{independent} from
+       a monitor and may occur freely. 
+*}
+
+
+doc_class article = 
+   T     :: "title option"     -- None
+   ST    :: "subtitle option"  -- None
+   AS    :: "author list"
+   ABS   :: "abstract option"
+   INTRO :: "introduction option" 
+   TS    :: "tech_section list"
+   EXS   :: "example_section list"
+   CON   :: "conclusion"
+   where "(title . 
+           [subtitle] .
+           (author)+ .
+           abstract .
+           introduction . 
+           (tech_section)+ . 
+           conclusion . 
+           bibliography)"
+
+-- \<open>other idea: capture the essence of a monitor class as trace.
+                trace would be `predefined id` like `main` in C.
+   \<close>
+
+doc_class article' = 
+   trace :: "(title + subtitle + author+ abstract +
+              introduction + tech_section + example_section +
+              conclusion + bibliography) list"
+   where "(title . 
+           [subtitle] .
+           (author)+ .
+           abstract .
+           introduction . 
+           (tech_section | example_section)+ . 
+           conclusion . 
+           bibliography)"
+
+
+
+end
+