equal
deleted
inserted
replaced
75 val mk_nchotomyN: string -> string |
75 val mk_nchotomyN: string -> string |
76 val mk_set_simpsN: int -> string |
76 val mk_set_simpsN: int -> string |
77 val mk_set_minimalN: int -> string |
77 val mk_set_minimalN: int -> string |
78 val mk_set_inductN: int -> string |
78 val mk_set_inductN: int -> string |
79 |
79 |
80 val typedef: bool -> binding option -> binding * (string * sort) list * mixfix -> term -> |
|
81 (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory |
|
82 |
|
83 val split_conj_thm: thm -> thm list |
80 val split_conj_thm: thm -> thm list |
84 val split_conj_prems: int -> thm -> thm |
81 val split_conj_prems: int -> thm -> thm |
85 |
82 |
86 val Inl_const: typ -> typ -> term |
83 val Inl_const: typ -> typ -> term |
87 val Inr_const: typ -> typ -> term |
84 val Inr_const: typ -> typ -> term |
123 |
120 |
124 val timing = true; |
121 val timing = true; |
125 fun time timer msg = (if timing |
122 fun time timer msg = (if timing |
126 then warning (msg ^ ": " ^ ATP_Util.string_from_time (Timer.checkRealTimer timer)) |
123 then warning (msg ^ ": " ^ ATP_Util.string_from_time (Timer.checkRealTimer timer)) |
127 else (); Timer.startRealTimer ()); |
124 else (); Timer.startRealTimer ()); |
128 |
|
129 (*TODO: is this really different from Typedef.add_typedef_global?*) |
|
130 fun typedef def opt_name typ set opt_morphs tac lthy = |
|
131 let |
|
132 val ((name, info), (lthy, lthy_old)) = |
|
133 lthy |
|
134 |> Typedef.add_typedef def opt_name typ set opt_morphs tac |
|
135 ||> `Local_Theory.restore; |
|
136 val phi = Proof_Context.export_morphism lthy_old lthy; |
|
137 in |
|
138 ((name, Typedef.transform_info phi info), lthy) |
|
139 end; |
|
140 |
125 |
141 val preN = "pre_" |
126 val preN = "pre_" |
142 val rawN = "raw_" |
127 val rawN = "raw_" |
143 |
128 |
144 val coN = "co" |
129 val coN = "co" |