equal
deleted
inserted
replaced
11 |
11 |
12 (* wrappers for define, note and theorem_i *) |
12 (* wrappers for define, note and theorem_i *) |
13 fun define (name, mx, rhs) lthy = |
13 fun define (name, mx, rhs) lthy = |
14 let |
14 let |
15 val ((rhs, (_ , thm)), lthy') = |
15 val ((rhs, (_ , thm)), lthy') = |
16 LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, rhs)) lthy |
16 Local_Theory.define "" ((name, mx), (Attrib.empty_binding, rhs)) lthy |
17 in |
17 in |
18 ((rhs, thm), lthy') |
18 ((rhs, thm), lthy') |
19 end |
19 end |
20 |
20 |
21 fun note (name, thm) lthy = |
21 fun note (name, thm) lthy = |
22 let |
22 let |
23 val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy |
23 val ((_,[thm']), lthy') = Local_Theory.note ((name, []), [thm]) lthy |
24 in |
24 in |
25 (thm', lthy') |
25 (thm', lthy') |
26 end |
26 end |
27 |
27 |
28 fun theorem after_qed goals ctxt = |
28 fun theorem after_qed goals ctxt = |
57 rtac @{thm exI}, |
57 rtac @{thm exI}, |
58 rtac @{thm exI}, |
58 rtac @{thm exI}, |
59 rtac @{thm refl}] |
59 rtac @{thm refl}] |
60 val tfrees = map fst (Term.add_tfreesT rty []) |
60 val tfrees = map fst (Term.add_tfreesT rty []) |
61 in |
61 in |
62 LocalTheory.theory_result |
62 Local_Theory.theory_result |
63 (Typedef.add_typedef false NONE |
63 (Typedef.add_typedef false NONE |
64 (qty_name, tfrees, mx) |
64 (qty_name, tfrees, mx) |
65 (typedef_term rel rty lthy) |
65 (typedef_term rel rty lthy) |
66 NONE typedef_tac) lthy |
66 NONE typedef_tac) lthy |
67 end |
67 end |
170 Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))] |
170 Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))] |
171 in |
171 in |
172 lthy5 |
172 lthy5 |
173 |> note (quot_thm_name, quot_thm) |
173 |> note (quot_thm_name, quot_thm) |
174 ||>> note (quotient_thm_name, quotient_thm) |
174 ||>> note (quotient_thm_name, quotient_thm) |
175 ||> LocalTheory.theory (fn thy => |
175 ||> Local_Theory.theory (fn thy => |
176 let |
176 let |
177 val global_eqns = map exp_term [eqn2i, eqn1i]; |
177 val global_eqns = map exp_term [eqn2i, eqn1i]; |
178 (* Not sure if the following context should not be used *) |
178 (* Not sure if the following context should not be used *) |
179 val (global_eqns2, lthy6) = Variable.import_terms true global_eqns lthy5; |
179 val (global_eqns2, lthy6) = Variable.import_terms true global_eqns lthy5; |
180 val global_eqns3 = map (fn t => (bindd, t)) global_eqns2; |
180 val global_eqns3 = map (fn t => (bindd, t)) global_eqns2; |