Lines Matching defs:Theory
2 (* FILE : Theory.sml *)
49 structure Theory :> Theory =
58 fun DPRINT f = if !debug then print ("Theory.DEBUG: " ^ f ()) else ()
59 val _ = register_btrace("Theory.debug", debug)
64 val ERR = mk_HOL_ERR "Theory";
65 val WARN = HOL_WARNING "Theory";
89 "Theory"
95 "Theory"
124 [] => HOL_WARNING "Theory" "delete_hook" ("No hook with name: "^nm)
608 val _ = Feedback.register_trace ("Theory.save_thm_reporting",
706 Theory data functions
852 ("Theory data name " ^ Lib.quote thydataty ^
959 val name = thyname^"Theory"
1017 (mesg ("Theory "^Lib.quote thyname^" took "^ tstr ^ " to build\n");
1213 handle e => raise (wrap_exn "Theory.Definition" "new_type_definition" e);
1258 end (* Theory *)