1structure HolKernel = 2struct 3 open HolKernel Logging 4 fun new_theory s = let 5 val _ = HolKernel.new_theory s 6 val _ = start_logging s 7 fun th {Thy,Tyop} = 8 case (Thy,Tyop) of 9 ("min", "fun") => ([], "->") 10 | ("min", "bool") => ([], "bool") 11 | _ => (["HOL4",Thy],Tyop) 12 fun ch {Thy,Name} = 13 case (Thy,Name) of 14 ("min", "=") => ([], "=") 15 | ("arithmetic", "NUMERAL") => (["Unwanted"],"id") 16 | _ => (["HOL4",Thy],Name) 17 val _ = set_tyop_name_handler th 18 val _ = set_const_name_handler ch 19 in () end 20 21 fun export_theory() = let 22 open Lib Theory 23 val directives = Logging.read_otdfile (current_theory() ^ ".otd") 24 handle IO.Io _ => [] 25 fun prepare (nm, th) = 26 (if Lib.mem (DeleteProof, nm) directives 27 then Thm.delete_proof th else (); 28 if Lib.mem (SkipThm, nm) directives 29 then NONE else SOME th) 30 val defs' = List.mapPartial prepare (current_definitions()) 31 val ths' = List.mapPartial prepare (current_theorems()) 32 val axs' = List.mapPartial prepare (current_axioms()) 33 val _ = List.app (ignore o export_thm) defs' 34 val _ = List.app (ignore o export_thm) ths' 35 val _ = List.app (ignore o export_thm) axs' 36 val _ = stop_logging() 37 in () end 38end 39