- tinkering ROOT

- activation of RegExps.

Isa_DOF.thy

@@ -49,7 +49,7 @@ term "@{term ''Bound 0''}"
 term "@{thm  ''refl''}"  
 term "@{docitem  ''<doc_ref>''}"
   
-type_synonym monitor = "int rexp"  
+  
   
 section{*Primitive Markup Generators*}
 ML{*
@@ -732,14 +732,11 @@ fun add_doc_class_cmd overloaded (raw_params, binding) raw_parent raw_fieldsNdef
                                                    else error("no overloading allowed.")
       val gen_antiquotation = OntoLinkParser.docitem_ref_antiquotation
       val _ = map_filter (check_n_filter thy) fields
-      val H = Sign.add_consts_cmd [(binding,"monitor",Mixfix.NoSyn)]
    
     in thy |> Record.add_record overloaded (params', binding) parent (tag_attr::fields) 
            |> DOF_core.define_doc_class_global (params', binding) parent fieldsNterms'
            |> (fn thy => gen_antiquotation binding (cid thy) thy) 
               (* defines the ontology-checked text antiquotation to this document class *)
-           |> Sign.add_consts_cmd [(binding,"monitor",Mixfix.NoSyn)]
-              (* defines syntax for monitor regeexpr for this class *)
     end;
 
 

ROOT

@@ -6,64 +6,3 @@ session "Isabelle_DOF" = HOL +
     Isa_DOF
 
 
-
-(*
- Bit
- Bits
- Boolean_Algebra
- Code_Abstract_Nat
- Code_Target_Nat
- Code_Target_Int
- Misc_Numeric
- Misc_Typedef
- Code_Target_Numeral
- Bit_Representation
- Bits_Bit
- Phantom_Type
- RegExp
- Word_Miscellaneous
- Bits_Int
- Cardinality
- Isa_MOF
- Numeral_Type
- Bool_List_Representation
- Type_Length
- Word
- Isa_DOF
- CENELEC_50126
-*)
-
-session "HOL-Analysis-AutoCorres" = "HOL-Analysis" +
-  theories [document=false]
-    "autocorres-1.3/autocorres/AutoCorres"
-
-
-session "Odo" = "HOL-Analysis-AutoCorres" +
-  description {* The Toplevel Requirement Documents of the Odometrie Service *}
-  options [document = pdf,document_variants="document:outline=/proof,/ML",document_output=output,quick_and_dirty]
-  theories [document=false]
-    "ontology_support/CENELEC_50126"
-    "Real"
-    "~~/src/HOL/Word/Word"
-    "Monads"
-    "Assert"
-  theories
-    "Odo_ReqAna"
-    "Odo_Design"
-  document_files
-     "root.tex"
-     "root.bib"
-     "main.tex"
-     "titlepage.tex"
-
-(* examples of s.th. more complex: 
-session "HOL-TestGen" (main) = "HOL-TestGenLib" +
-  description {* HOL-TestGen *}
-  theories 
-    "codegen_fsharp/Code_String_Fsharp"
-    "codegen_fsharp/Code_Char_chr_Fsharp"
-    "codegen_fsharp/Code_Integer_Fsharp" 
-    "codegen_fsharp/Code_Char_Fsharp"
-    "Testing"
-    "IOCO"
-*)