src/postkernel/Theory.sml

2 (* FILE          : Theory.sml                                                *)
49 structure Theory :> Theory =
60 val ERR  = mk_HOL_ERR "Theory";
61 val WARN = HOL_WARNING "Theory";
85                "Theory"
91                "Theory"
120     [] => HOL_WARNING "Theory" "delete_hook" ("No hook with name: "^nm)
591   val _ = Feedback.register_trace ("Theory.save_thm_reporting",
689     Theory data functions
802                     ("Theory data name " ^ Lib.quote thydataty ^
907   val name = thyname^"Theory"
962           (mesg ("Theory "^Lib.quote thyname^" took "^ tstr ^ " to build\n");
1158  handle e => raise (wrap_exn "Theory.Definition" "new_type_definition" e);
1203 end (* Theory *)