198 |
198 |
199 |
199 |
200 (* store axioms as theorems *) |
200 (* store axioms as theorems *) |
201 |
201 |
202 local |
202 local |
203 fun add_axm add = fold_map (fn ((b, prop), atts) => fn thy => |
203 |
204 let |
204 fun no_read _ (_, t) = t; |
205 val thy' = add [(b, prop)] thy; |
205 |
206 val thm = Thm.forall_elim_vars 0 (Thm.axiom thy' (Sign.full_name thy' b)); |
206 fun read thy (b, str) = |
207 in apfst hd (gen_add_thms (K I) [((b, thm), atts)] thy') end); |
207 Syntax.read_prop_global thy str handle ERROR msg => |
|
208 cat_error msg ("The error(s) above occurred in definition " ^ quote (Binding.str_of b)); |
|
209 |
|
210 fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy => |
|
211 let |
|
212 val prop = prep thy (b, raw_prop); |
|
213 val (def, thy') = Thm.add_def unchecked overloaded (b, prop) thy; |
|
214 val thm = def |
|
215 |> Thm.forall_intr_frees |
|
216 |> Thm.forall_elim_vars 0 |
|
217 |> Thm.varifyT_global; |
|
218 in yield_singleton (gen_add_thms (K I)) ((b, thm), atts) thy' end); |
|
219 |
208 in |
220 in |
209 val add_defs = add_axm o Theory.add_defs_i false; |
221 |
210 val add_defs_unchecked = add_axm o Theory.add_defs_i true; |
222 val add_defs = add no_read false; |
211 val add_defs_cmd = add_axm o Theory.add_defs false; |
223 val add_defs_unchecked = add no_read true; |
212 val add_defs_unchecked_cmd = add_axm o Theory.add_defs true; |
224 val add_defs_cmd = add read false; |
|
225 val add_defs_unchecked_cmd = add read true; |
|
226 |
213 end; |
227 end; |
214 |
228 |
215 |
229 |
216 |
230 |
217 (*** Pure theory syntax and logical content ***) |
231 (*** Pure theory syntax and logical content ***) |