--- a/src/HOL/Hyperreal/transfer.ML Sun Jul 29 14:29:52 2007 +0200
+++ b/src/HOL/Hyperreal/transfer.ML Sun Jul 29 14:29:54 2007 +0200
@@ -30,14 +30,12 @@
refolds = refolds1, consts = consts1},
{intros = intros2, unfolds = unfolds2,
refolds = refolds2, consts = consts2}) =
- {intros = Drule.merge_rules (intros1, intros2),
- unfolds = Drule.merge_rules (unfolds1, unfolds2),
- refolds = Drule.merge_rules (refolds1, refolds2),
+ {intros = Thm.merge_thms (intros1, intros2),
+ unfolds = Thm.merge_thms (unfolds1, unfolds2),
+ refolds = Thm.merge_thms (refolds1, refolds2),
consts = Library.merge (op =) (consts1, consts2)} : T;
);
-val transfer_start = thm "transfer_start"
-
fun unstar_typ (Type ("StarDef.star",[t])) = unstar_typ t
| unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts)
| unstar_typ T = T
@@ -48,7 +46,7 @@
else (Const(a,unstar_typ T) $ unstar t)
| unstar (f $ t) = unstar f $ unstar t
| unstar (Const(a,T)) = Const(a,unstar_typ T)
- | unstar (Abs(a,T,t)) = Abs(a,unstar_typ T,unstar t)
+ | unstar (Abs(a,T,t)) = Abs(a,unstar_typ T,unstar t)
| unstar t = t
in
unstar term
@@ -67,7 +65,7 @@
rewrite_goals_tac (ths' @ refolds' @ unfolds') THEN
ALLGOALS ObjectLogic.full_atomize_tac THEN
match_tac [transitive_thm] 1 THEN
- resolve_tac [transfer_start] 1 THEN
+ resolve_tac [@{thm transfer_start}] 1 THEN
REPEAT_ALL_NEW (resolve_tac intros) 1 THEN
match_tac [reflexive_thm] 1
in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end
@@ -92,14 +90,14 @@
(fn {intros,unfolds,refolds,consts} =>
{intros=intros, unfolds=unfolds, refolds=f refolds, consts=consts})
in
-val intro_add = Thm.declaration_attribute (map_intros o Drule.add_rule);
-val intro_del = Thm.declaration_attribute (map_intros o Drule.del_rule);
+val intro_add = Thm.declaration_attribute (map_intros o Thm.add_thm);
+val intro_del = Thm.declaration_attribute (map_intros o Thm.del_thm);
-val unfold_add = Thm.declaration_attribute (map_unfolds o Drule.add_rule);
-val unfold_del = Thm.declaration_attribute (map_unfolds o Drule.del_rule);
+val unfold_add = Thm.declaration_attribute (map_unfolds o Thm.add_thm);
+val unfold_del = Thm.declaration_attribute (map_unfolds o Thm.del_thm);
-val refold_add = Thm.declaration_attribute (map_refolds o Drule.add_rule);
-val refold_del = Thm.declaration_attribute (map_refolds o Drule.del_rule);
+val refold_add = Thm.declaration_attribute (map_refolds o Thm.add_thm);
+val refold_del = Thm.declaration_attribute (map_refolds o Thm.del_thm);
end
fun add_const c = Context.theory_map (TransferData.map
--- a/src/HOL/Nominal/nominal_thmdecls.ML Sun Jul 29 14:29:52 2007 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Sun Jul 29 14:29:54 2007 +0200
@@ -34,9 +34,9 @@
type T = {eqvts:thm list, freshs:thm list, bijs:thm list};
val empty = ({eqvts=[], freshs=[], bijs=[]}:T);
val extend = I;
- fun merge _ (r1:T,r2:T) = {eqvts = Drule.merge_rules (#eqvts r1, #eqvts r2),
- freshs = Drule.merge_rules (#freshs r1, #freshs r2),
- bijs = Drule.merge_rules (#bijs r1, #bijs r2)}
+ fun merge _ (r1:T,r2:T) = {eqvts = Thm.merge_thms (#eqvts r1, #eqvts r2),
+ freshs = Thm.merge_thms (#freshs r1, #freshs r2),
+ bijs = Thm.merge_thms (#bijs r1, #bijs r2)}
);
(* Exception for when a theorem does not conform with form of an equivariance lemma. *)
@@ -102,7 +102,7 @@
val lhs = (Const("Nominal.perm", typi --> HOLogic.boolT --> HOLogic.boolT) $ Var(pi,typi) $ hyp)
val goal_term = Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,concl)))
val _ = Display.print_cterm (cterm_of thy goal_term)
- in
+ in
Goal.prove_global thy [] [] goal_term (fn _ => (tactic_eqvt thy orig_thm pi typi))
end
@@ -136,10 +136,10 @@
(Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $
(Var (n,ty))) =>
let
- (* FIXME: this should be an operation the library *)
+ (* FIXME: this should be an operation the library *)
val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm)
- in
- if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name]))
+ in
+ if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name]))
then [(pi,typi)]
else raise
EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name)
@@ -177,7 +177,7 @@
(* case: eqvt-lemma is of the equational form *)
| (Const ("Trueprop", _) $ (Const ("op =", _) $
(Const ("Nominal.perm",typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
- (if (apply_pi lhs (pi,typi)) = rhs
+ (if (apply_pi lhs (pi,typi)) = rhs
then [orig_thm]
else raise EQVT_FORM "Type Equality")
| _ => raise EQVT_FORM "Type unknown")
@@ -205,15 +205,15 @@
fun fresh_map f th (r:Data.T) = {eqvts = #eqvts r, freshs = (f th (#freshs r)), bijs = #bijs r};
fun bij_map f th (r:Data.T) = {eqvts = #eqvts r, freshs = #freshs r, bijs = (f th (#bijs r))};
-val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.add_rule));
-val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.del_rule));
-val eqvt_force_add = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.add_rule));
-val eqvt_force_del = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.del_rule));
+val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Thm.add_thm));
+val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Thm.del_thm));
+val eqvt_force_add = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Thm.add_thm));
+val eqvt_force_del = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Thm.del_thm));
-val bij_add = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.add_rule));
-val bij_del = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.del_rule));
-val fresh_add = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.add_rule));
-val fresh_del = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.del_rule));
+val bij_add = Thm.declaration_attribute (bij_add_del_aux (bij_map Thm.add_thm));
+val bij_del = Thm.declaration_attribute (bij_add_del_aux (bij_map Thm.del_thm));
+val fresh_add = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Thm.add_thm));
+val fresh_del = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Thm.del_thm));
@@ -221,7 +221,7 @@
Attrib.add_attributes
[("eqvt", Attrib.add_del_args eqvt_add eqvt_del, "equivariance theorem declaration"),
("eqvt_force", Attrib.add_del_args eqvt_force_add eqvt_force_del,
- "equivariance theorem declaration (without checking the form of the lemma)"),
+ "equivariance theorem declaration (without checking the form of the lemma)"),
("fresh", Attrib.add_del_args fresh_add fresh_del, "freshness theorem declaration"),
("bij", Attrib.add_del_args bij_add bij_del, "bijection theorem declaration")];
--- a/src/HOL/Tools/function_package/fundef_common.ML Sun Jul 29 14:29:52 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML Sun Jul 29 14:29:54 2007 +0200
@@ -89,7 +89,7 @@
type T = thm list
val empty = []
val extend = I
- fun merge _ = Drule.merge_rules
+ fun merge _ = Thm.merge_thms
);
@@ -136,7 +136,7 @@
type T = thm list
val empty = []
val extend = I
- fun merge _ = Drule.merge_rules
+ fun merge _ = Thm.merge_thms
);
val get_termination_rules = TerminationRule.get
--- a/src/HOL/Tools/function_package/fundef_package.ML Sun Jul 29 14:29:52 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML Sun Jul 29 14:29:54 2007 +0200
@@ -172,14 +172,14 @@
(* congruence rules *)
-val cong_add = Thm.declaration_attribute (map_fundef_congs o Drule.add_rule o safe_mk_meta_eq);
-val cong_del = Thm.declaration_attribute (map_fundef_congs o Drule.del_rule o safe_mk_meta_eq);
+val cong_add = Thm.declaration_attribute (map_fundef_congs o Thm.add_thm o safe_mk_meta_eq);
+val cong_del = Thm.declaration_attribute (map_fundef_congs o Thm.del_thm o safe_mk_meta_eq);
(* Datatype hook to declare datatype congs as "fundef_congs" *)
fun add_case_cong n thy =
- Context.theory_map (map_fundef_congs (Drule.add_rule
+ Context.theory_map (map_fundef_congs (Thm.add_thm
(DatatypePackage.get_datatype thy n |> the
|> #case_cong
|> safe_mk_meta_eq)))
--- a/src/HOL/Tools/inductive_package.ML Sun Jul 29 14:29:52 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML Sun Jul 29 14:29:54 2007 +0200
@@ -134,7 +134,7 @@
val empty = (Symtab.empty, []);
val extend = I;
fun merge _ ((tab1, monos1), (tab2, monos2)) =
- (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
+ (Symtab.merge (K true) (tab1, tab2), Thm.merge_thms (monos1, monos2));
);
val get_inductives = InductiveData.get o Context.Proof;
@@ -187,8 +187,8 @@
| _ => [thm]
end handle THM _ => error ("Bad monotonicity theorem:\n" ^ string_of_thm thm);
-val mono_add = Thm.declaration_attribute (map_monos o fold Drule.add_rule o mk_mono);
-val mono_del = Thm.declaration_attribute (map_monos o fold Drule.del_rule o mk_mono);
+val mono_add = Thm.declaration_attribute (map_monos o fold Thm.add_thm o mk_mono);
+val mono_del = Thm.declaration_attribute (map_monos o fold Thm.del_thm o mk_mono);
--- a/src/HOL/Tools/inductive_set_package.ML Sun Jul 29 14:29:52 2007 +0200
+++ b/src/HOL/Tools/inductive_set_package.ML Sun Jul 29 14:29:54 2007 +0200
@@ -172,8 +172,8 @@
set_arities = set_arities1, pred_arities = pred_arities1},
{to_set_simps = to_set_simps2, to_pred_simps = to_pred_simps2,
set_arities = set_arities2, pred_arities = pred_arities2}) =
- {to_set_simps = Drule.merge_rules (to_set_simps1, to_set_simps2),
- to_pred_simps = Drule.merge_rules (to_pred_simps1, to_pred_simps2),
+ {to_set_simps = Thm.merge_thms (to_set_simps1, to_set_simps2),
+ to_pred_simps = Thm.merge_thms (to_pred_simps1, to_pred_simps2),
set_arities = Symtab.merge_list op = (set_arities1, set_arities2),
pred_arities = Symtab.merge_list op = (pred_arities1, pred_arities2)};
);
--- a/src/HOL/Tools/recdef_package.ML Sun Jul 29 14:29:52 2007 +0200
+++ b/src/HOL/Tools/recdef_package.ML Sun Jul 29 14:29:54 2007 +0200
@@ -105,9 +105,9 @@
((tab1, {simps = simps1, congs = congs1, wfs = wfs1}),
(tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T =
(Symtab.merge (K true) (tab1, tab2),
- mk_hints (Drule.merge_rules (simps1, simps2),
+ mk_hints (Thm.merge_thms (simps1, simps2),
AList.merge (op =) Thm.eq_thm (congs1, congs2),
- Drule.merge_rules (wfs1, wfs2)));
+ Thm.merge_thms (wfs1, wfs2)));
);
val get_recdef = Symtab.lookup o #1 o GlobalRecdefData.get;
@@ -138,12 +138,12 @@
fun attrib f = Thm.declaration_attribute (map_hints o f);
-val simp_add = attrib (map_simps o Drule.add_rule);
-val simp_del = attrib (map_simps o Drule.del_rule);
+val simp_add = attrib (map_simps o Thm.add_thm);
+val simp_del = attrib (map_simps o Thm.del_thm);
val cong_add = attrib (map_congs o add_cong);
val cong_del = attrib (map_congs o del_cong);
-val wf_add = attrib (map_wfs o Drule.add_rule);
-val wf_del = attrib (map_wfs o Drule.del_rule);
+val wf_add = attrib (map_wfs o Thm.add_thm);
+val wf_del = attrib (map_wfs o Thm.del_thm);
(* modifiers *)
--- a/src/Provers/Arith/fast_lin_arith.ML Sun Jul 29 14:29:52 2007 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Sun Jul 29 14:29:54 2007 +0200
@@ -122,11 +122,11 @@
lessD = lessD1, neqE=neqE1, simpset = simpset1},
{add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2,
lessD = lessD2, neqE=neqE2, simpset = simpset2}) =
- {add_mono_thms = Drule.merge_rules (add_mono_thms1, add_mono_thms2),
- mult_mono_thms = Drule.merge_rules (mult_mono_thms1, mult_mono_thms2),
- inj_thms = Drule.merge_rules (inj_thms1, inj_thms2),
- lessD = Drule.merge_rules (lessD1, lessD2),
- neqE = Drule.merge_rules (neqE1, neqE2),
+ {add_mono_thms = Thm.merge_thms (add_mono_thms1, add_mono_thms2),
+ mult_mono_thms = Thm.merge_thms (mult_mono_thms1, mult_mono_thms2),
+ inj_thms = Thm.merge_thms (inj_thms1, inj_thms2),
+ lessD = Thm.merge_thms (lessD1, lessD2),
+ neqE = Thm.merge_thms (neqE1, neqE2),
simpset = Simplifier.merge_ss (simpset1, simpset2)};
);
--- a/src/Pure/Isar/calculation.ML Sun Jul 29 14:29:52 2007 +0200
+++ b/src/Pure/Isar/calculation.ML Sun Jul 29 14:29:54 2007 +0200
@@ -35,7 +35,7 @@
val extend = I;
fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) =
- ((NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2)), NONE);
+ ((NetRules.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE);
);
fun print_rules ctxt =
@@ -71,10 +71,10 @@
val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.delete);
val sym_add =
- Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Drule.add_rule)
+ Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm)
#> ContextRules.elim_query NONE;
val sym_del =
- Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Drule.del_rule)
+ Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.del_thm)
#> ContextRules.rule_del;
--- a/src/Pure/Isar/local_defs.ML Sun Jul 29 14:29:52 2007 +0200
+++ b/src/Pure/Isar/local_defs.ML Sun Jul 29 14:29:54 2007 +0200
@@ -151,15 +151,15 @@
type T = thm list;
val empty = []
val extend = I;
- fun merge _ = Drule.merge_rules;
+ fun merge _ = Thm.merge_thms;
);
fun print_rules ctxt =
Pretty.writeln (Pretty.big_list "definitional transformations:"
(map (ProofContext.pretty_thm ctxt) (Rules.get (Context.Proof ctxt))));
-val defn_add = Thm.declaration_attribute (Rules.map o Drule.add_rule);
-val defn_del = Thm.declaration_attribute (Rules.map o Drule.del_rule);
+val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm);
+val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm);
(* meta rewrite rules *)
--- a/src/Pure/Isar/object_logic.ML Sun Jul 29 14:29:52 2007 +0200
+++ b/src/Pure/Isar/object_logic.ML Sun Jul 29 14:29:54 2007 +0200
@@ -51,7 +51,7 @@
fun merge _ ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) =
(merge_judgment (judgment1, judgment2),
- (Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2)));
+ (Thm.merge_thms (atomize1, atomize2), Thm.merge_thms (rulify1, rulify2)));
);
@@ -141,8 +141,8 @@
val get_atomize = #1 o #2 o ObjectLogicData.get;
val get_rulify = #2 o #2 o ObjectLogicData.get;
-val add_atomize = ObjectLogicData.map o apsnd o apfst o Drule.add_rule;
-val add_rulify = ObjectLogicData.map o apsnd o apsnd o Drule.add_rule;
+val add_atomize = ObjectLogicData.map o apsnd o apfst o Thm.add_thm;
+val add_rulify = ObjectLogicData.map o apsnd o apsnd o Thm.add_thm;
val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);
--- a/src/ZF/Tools/typechk.ML Sun Jul 29 14:29:52 2007 +0200
+++ b/src/ZF/Tools/typechk.ML Sun Jul 29 14:29:54 2007 +0200
@@ -49,7 +49,7 @@
val extend = I;
fun merge _ (TC {rules, net}, TC {rules = rules', net = net'}) =
- TC {rules = Drule.merge_rules (rules, rules'),
+ TC {rules = Thm.merge_thms (rules, rules'),
net = Net.merge Thm.eq_thm_prop (net, net')};
);