--- a/src/HOL/Fun.thy Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Fun.thy Fri Mar 07 22:30:58 2014 +0100
@@ -895,7 +895,7 @@
SOME (Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs))
(fn _ =>
rtac eq_reflection 1 THEN
- rtac ext 1 THEN
+ rtac @{thm ext} 1 THEN
simp_tac (put_simpset ss ctxt) 1))
end
in proc end
--- a/src/HOL/Nominal/nominal_datatype.ML Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Fri Mar 07 22:30:58 2014 +0100
@@ -1723,8 +1723,8 @@
(finite_thss ~~ finite_ctxt_ths) @
maps (fn ((_, idxss), elim) => maps (fn idxs =>
[full_simp_tac (put_simpset HOL_ss context addsimps [Thm.symmetric fresh_def, supp_prod, Un_iff]) 1,
- REPEAT_DETERM (eresolve_tac [conjE, ex1E] 1),
- rtac ex1I 1,
+ REPEAT_DETERM (eresolve_tac @{thms conjE ex1E} 1),
+ rtac @{thm ex1I} 1,
(resolve_tac rec_intrs THEN_ALL_NEW atac) 1,
rotate_tac ~1 1,
((DETERM o etac elim) THEN_ALL_NEW full_simp_tac
--- a/src/HOL/Nominal/nominal_permeq.ML Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML Fri Mar 07 22:30:58 2014 +0100
@@ -241,7 +241,7 @@
(* applies the ext-rule such that *)
(* *)
(* f = g goes to /\x. f x = g x *)
-fun ext_fun_tac i = ("extensionality expansion of functions", rtac ext i);
+fun ext_fun_tac i = ("extensionality expansion of functions", rtac @{thm ext} i);
(* perm_extend_simp_tac_i is perm_simp plus additional tactics *)
--- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML Fri Mar 07 22:30:58 2014 +0100
@@ -55,17 +55,17 @@
rtac refl 1;
fun mk_comp_map_id0_tac Gmap_id0 Gmap_cong0 map_id0s =
- EVERY' ([rtac ext, rtac (Gmap_cong0 RS trans)] @
+ EVERY' ([rtac @{thm ext}, rtac (Gmap_cong0 RS trans)] @
map (fn thm => rtac (thm RS fun_cong)) map_id0s @ [rtac (Gmap_id0 RS fun_cong)]) 1;
fun mk_comp_map_comp0_tac Gmap_comp0 Gmap_cong0 map_comp0s =
- EVERY' ([rtac ext, rtac sym, rtac trans_o_apply,
+ EVERY' ([rtac @{thm ext}, rtac sym, rtac trans_o_apply,
rtac (Gmap_comp0 RS sym RS comp_eq_dest_lhs RS trans), rtac Gmap_cong0] @
map (fn thm => rtac (thm RS sym RS fun_cong)) map_comp0s) 1;
fun mk_comp_set_map0_tac ctxt set'_eq_set Gmap_comp0 Gmap_cong0 Gset_map0 set_map0s =
unfold_thms_tac ctxt [set'_eq_set] THEN
- EVERY' ([rtac ext] @
+ EVERY' ([rtac @{thm ext}] @
replicate 3 (rtac trans_o_apply) @
[rtac (arg_cong_Union RS trans),
rtac (@{thm arg_cong2[of _ _ _ _ collect, OF refl]} RS trans),
@@ -79,7 +79,7 @@
rtac @{thm trans[OF comp_eq_dest_lhs[OF image_o_collect[symmetric]]]},
rtac @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @
[REPEAT_DETERM_N (length set_map0s) o EVERY' [rtac @{thm trans[OF image_insert]},
- rtac @{thm arg_cong2[of _ _ _ _ insert]}, rtac ext, rtac trans_o_apply,
+ rtac @{thm arg_cong2[of _ _ _ _ insert]}, rtac @{thm ext}, rtac trans_o_apply,
rtac trans_image_cong_o_apply, rtac @{thm trans[OF image_image]},
rtac @{thm sym[OF trans[OF o_apply]]}, rtac @{thm image_cong[OF refl o_apply]}],
rtac @{thm image_empty}]) 1;
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Fri Mar 07 22:30:58 2014 +0100
@@ -84,7 +84,8 @@
hyp_subst_tac ctxt,
rtac @{thm relcomppI}, rtac @{thm conversepI},
EVERY' (map2 (fn convol => fn map_id0 =>
- EVERY' [rtac @{thm GrpI}, rtac (box_equals OF [map_cong0, map_comp RS sym, map_id0]),
+ EVERY' [rtac @{thm GrpI},
+ rtac (@{thm box_equals} OF [map_cong0, map_comp RS sym, map_id0]),
REPEAT_DETERM_N n o rtac (convol RS fun_cong),
REPEAT_DETERM o eresolve_tac [CollectE, conjE],
rtac CollectI,
@@ -203,7 +204,7 @@
rtac @{thm vimage2pI}, rtac (in_rel RS iffD2), rtac exI, rtac conjI, in_tac,
rtac conjI,
EVERY' (map (fn convol =>
- rtac (box_equals OF [map_cong0, map_comp RS sym, map_comp RS sym]) THEN'
+ rtac (@{thm box_equals} OF [map_cong0, map_comp RS sym, map_comp RS sym]) THEN'
REPEAT_DETERM_N n o rtac (convol RS fun_cong)) @{thms fst_convol snd_convol})])
end;
@@ -254,7 +255,7 @@
(K (etac @{thm If_the_inv_into_in_Func} THEN' atac)) set_maps,
rtac sym,
rtac (Drule.rotate_prems 1
- ((box_equals OF [map_cong0 OF replicate live @{thm If_the_inv_into_f_f},
+ ((@{thm box_equals} OF [map_cong0 OF replicate live @{thm If_the_inv_into_f_f},
map_comp RS sym, map_id]) RSN (2, trans))),
REPEAT_DETERM_N (2 * live) o atac,
REPEAT_DETERM_N live o rtac (@{thm prod.case} RS trans),
@@ -265,7 +266,7 @@
rtac (thm RS ord_eq_le_trans) THEN' etac @{thm subset_trans[OF image_mono Un_upper1]})
set_maps,
rtac sym,
- rtac (box_equals OF [map_cong0 OF replicate live @{thm fun_cong[OF case_sum_o_inj(1)]},
+ rtac (@{thm box_equals} OF [map_cong0 OF replicate live @{thm fun_cong[OF case_sum_o_inj(1)]},
map_comp RS sym, map_id])] 1
end;
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Mar 07 22:30:58 2014 +0100
@@ -525,7 +525,8 @@
val map_cong_active_args2 = replicate n (if is_rec
then case_fp fp @{thm map_prod_o_convol_id} @{thm case_sum_o_map_sum_id}
else case_fp fp @{thm id_comp} @{thm comp_id} RS fun_cong);
- fun mk_map_congs passive active = map (fn thm => thm OF (passive @ active) RS ext) map_cong0s;
+ fun mk_map_congs passive active =
+ map (fn thm => thm OF (passive @ active) RS @{thm ext}) map_cong0s;
val map_cong1s = mk_map_congs map_cong_passive_args1 map_cong_active_args1;
val map_cong2s = mk_map_congs map_cong_passive_args2 map_cong_active_args2;
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Fri Mar 07 22:30:58 2014 +0100
@@ -140,7 +140,7 @@
(CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
sum.case} @ mapsx @ map_comps @ map_idents))) ORELSE'
fo_rtac @{thm cong} ctxt ORELSE'
- rtac ext));
+ rtac @{thm ext}));
fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs =
HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN'
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Fri Mar 07 22:30:58 2014 +0100
@@ -145,7 +145,7 @@
fun mk_mor_UNIV_tac morEs mor_def =
let
val n = length morEs;
- fun mor_tac morE = EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, etac morE,
+ fun mor_tac morE = EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, etac morE,
rtac UNIV_I, rtac sym, rtac o_apply];
in
EVERY' [rtac iffI, CONJ_WRAP' mor_tac morEs,
@@ -201,7 +201,7 @@
(fn (rec_Suc, (morE, ((passive_set_map0s, active_set_map0s), coalg_sets))) =>
EVERY' [rtac impI, rtac (rec_Suc RS trans), rtac (rec_Suc RS trans RS sym),
if m = 0 then K all_tac
- else EVERY' [rtac Un_cong, rtac box_equals,
+ else EVERY' [rtac Un_cong, rtac @{thm box_equals},
rtac (nth passive_set_map0s (j - 1) RS sym),
rtac trans_fun_cong_image_id_id_apply, etac (morE RS arg_cong), atac],
CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 Un_cong))
@@ -637,7 +637,7 @@
ks to_sbd_injs from_to_sbds)];
in
(rtac mor_cong THEN'
- EVERY' (map (fn thm => rtac (thm RS ext)) beh_defs) THEN'
+ EVERY' (map (fn thm => rtac (thm RS @{thm ext})) beh_defs) THEN'
stac mor_def THEN' rtac conjI THEN'
CONJ_WRAP' fbetw_tac
(ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ ((length_Levs ~~ length_Lev's) ~~
@@ -702,7 +702,7 @@
fun mk_mor_unfold_tac m mor_UNIV dtor_defs unfold_defs Abs_inverses morEs map_comp_ids map_cong0s =
EVERY' [rtac iffD2, rtac mor_UNIV,
CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, unfold_def), (map_comp_id, map_cong0))) =>
- EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (dtor_def RS trans),
+ EVERY' [rtac @{thm ext}, rtac (o_apply RS trans RS sym), rtac (dtor_def RS trans),
rtac (unfold_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans),
rtac (morE RS arg_cong RS trans), rtac (map_comp_id RS trans),
rtac (o_apply RS trans RS sym), rtac map_cong0,
@@ -737,12 +737,12 @@
fun mk_unfold_unique_mor_tac raw_coinds bis mor unfold_defs =
CONJ_WRAP' (fn (raw_coind, unfold_def) =>
- EVERY' [rtac ext, etac (bis RS raw_coind RS set_mp RS @{thm IdD}), rtac mor,
+ EVERY' [rtac @{thm ext}, etac (bis RS raw_coind RS set_mp RS @{thm IdD}), rtac mor,
rtac @{thm image2_eqI}, rtac refl, rtac (unfold_def RS arg_cong RS trans),
rtac (o_apply RS sym), rtac UNIV_I]) (raw_coinds ~~ unfold_defs) 1;
fun mk_dtor_o_ctor_tac ctxt ctor_def unfold map_comp_id map_cong0L unfold_o_dtors =
- unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
+ unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply,
rtac trans, rtac unfold, rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L,
EVERY' (map (fn thm =>
rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply])) unfold_o_dtors),
@@ -774,8 +774,9 @@
rtac CollectI, etac @{thm case_prodI}])) rel_congs] 1;
fun mk_map_tac m n map_arg_cong unfold map_comp map_cong0 =
- EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym),
- rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp RS box_equals)), rtac map_cong0,
+ EVERY' [rtac @{thm ext}, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym),
+ rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp RS @{thm box_equals})),
+ rtac map_cong0,
REPEAT_DETERM_N m o rtac (@{thm id_comp} RS fun_cong),
REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),
rtac map_arg_cong, rtac (o_apply RS sym)] 1;
@@ -875,9 +876,9 @@
end;
fun mk_set_map0_tac hset_def col_natural =
- EVERY' (map rtac [ext, (o_apply RS trans), (hset_def RS trans), sym,
- (o_apply RS trans), (@{thm image_cong} OF [hset_def, refl] RS trans),
- (@{thm image_UN} RS trans), (refl RS @{thm UN_cong}), col_natural]) 1;
+ EVERY' (map rtac [@{thm ext}, o_apply RS trans, hset_def RS trans, sym,
+ o_apply RS trans, @{thm image_cong} OF [hset_def, refl] RS trans,
+ @{thm image_UN} RS trans, refl RS @{thm UN_cong}, col_natural]) 1;
fun mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss =
let
@@ -965,7 +966,7 @@
rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
CONJ_WRAP' (fn (dtor_set, passive_set_map0) =>
EVERY' [rtac ord_eq_le_trans, rtac dtor_set, rtac @{thm Un_least},
- rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_map0,
+ rtac ord_eq_le_trans, rtac @{thm box_equals}, rtac passive_set_map0,
rtac (dtor_ctor RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac,
CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
(fn (active_set_map0, in_Jrel) => EVERY' [rtac ord_eq_le_trans,
@@ -985,7 +986,7 @@
(dtor_sets ~~ passive_set_map0s),
rtac conjI,
REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map,
- rtac box_equals, rtac map_comp0, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
+ rtac @{thm box_equals}, rtac map_comp0, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]},
EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
dtac @{thm ssubst_mem[OF pair_collapse]},
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Fri Mar 07 22:30:58 2014 +0100
@@ -174,7 +174,7 @@
fun mk_mor_UNIV_tac m morEs mor_def =
let
val n = length morEs;
- fun mor_tac morE = EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, etac morE,
+ fun mor_tac morE = EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, etac morE,
rtac CollectI, CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto m + n),
rtac sym, rtac o_apply];
in
@@ -507,7 +507,7 @@
end;
fun mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_cong0L ctor_o_folds =
- EVERY' [stac dtor_def, rtac ext, rtac trans, rtac o_apply, rtac trans, rtac foldx,
+ EVERY' [stac dtor_def, rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, rtac foldx,
rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L,
EVERY' (map (fn thm => rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply]))
ctor_o_folds),
@@ -568,7 +568,8 @@
end;
fun mk_map_tac m n foldx map_comp_id map_cong0 =
- EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac foldx, rtac trans, rtac o_apply,
+ EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, rtac foldx, rtac trans,
+ rtac o_apply,
rtac trans, rtac (map_comp_id RS arg_cong), rtac trans, rtac (map_cong0 RS arg_cong),
REPEAT_DETERM_N m o rtac refl,
REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])),
@@ -579,7 +580,7 @@
unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc id_comp comp_id}) THEN
ALLGOALS atac;
-fun mk_set_tac foldx = EVERY' [rtac ext, rtac trans, rtac o_apply,
+fun mk_set_tac foldx = EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply,
rtac trans, rtac foldx, rtac sym, rtac o_apply] 1;
fun mk_ctor_set_tac set set_map set_maps =
@@ -674,7 +675,7 @@
val map_comp0s' = drop i map_comp0s @ take i map_comp0s;
val ctor_maps' = drop i ctor_maps @ take i ctor_maps;
fun mk_comp comp simp =
- EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac o_apply,
+ EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, rtac o_apply,
rtac trans, rtac (simp RS arg_cong), rtac trans, rtac simp,
rtac trans, rtac (comp RS arg_cong), rtac sym, rtac o_apply];
in
@@ -682,7 +683,7 @@
end;
fun mk_set_map0_tac set_nat =
- EVERY' (map rtac [ext, trans, o_apply, sym, trans, o_apply, set_nat]) 1;
+ EVERY' (map rtac [@{thm ext}, trans, o_apply, sym, trans, o_apply, set_nat]) 1;
fun mk_bd_card_order_tac bd_card_orders =
CONJ_WRAP_GEN' (rtac @{thm card_order_csum}) rtac bd_card_orders 1;
--- a/src/HOL/Tools/BNF/bnf_tactics.ML Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_tactics.ML Fri Mar 07 22:30:58 2014 +0100
@@ -47,7 +47,7 @@
|> pairself (dest_comb #> apsnd (dest_comb #> fst) #> HOLogic.mk_comp)
|> mk_Trueprop_eq
|> (fn goal => Goal.prove_sorry ctxt [] [] goal
- (K (rtac ext 1 THEN unfold_thms_tac ctxt [o_apply, mk_sym thm] THEN rtac refl 1)))
+ (K (rtac @{thm ext} 1 THEN unfold_thms_tac ctxt [o_apply, mk_sym thm] THEN rtac refl 1)))
|> Thm.close_derivation;
--- a/src/HOL/Tools/Datatype/datatype.ML Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Fri Mar 07 22:30:58 2014 +0100
@@ -382,7 +382,7 @@
(map (pair "x") Ts, S $ Datatype_Aux.app_bnds f i)),
HOLogic.mk_Trueprop (HOLogic.mk_eq (fold_rev (Term.abs o pair "x") Ts
(r $ (a $ Datatype_Aux.app_bnds f i)), f))))
- (fn _ => EVERY [REPEAT_DETERM_N i (rtac ext 1),
+ (fn _ => EVERY [REPEAT_DETERM_N i (rtac @{thm ext} 1),
REPEAT (etac allE 1), rtac thm 1, atac 1])
end
in map (fn r => r RS subst) (thm :: map mk_thm arities) end;
@@ -432,7 +432,7 @@
map make_elim [Leaf_inject, Inl_inject, Inr_inject]) 1),
REPEAT (cong_tac 1), rtac refl 1,
REPEAT (atac 1 ORELSE (EVERY
- [REPEAT (rtac ext 1),
+ [REPEAT (rtac @{thm ext} 1),
REPEAT (eresolve_tac (mp :: allE ::
map make_elim (Suml_inject :: Sumr_inject ::
Lim_inject :: inj_thms') @ fun_congs) 1),
@@ -487,7 +487,7 @@
Thm.symmetric (mk_meta_eq @{thm fun_eq_iff}) :: range_eqs),
rewrite_goals_tac ctxt (map Thm.symmetric range_eqs),
REPEAT (EVERY
- [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
+ [REPEAT (eresolve_tac ([rangeE, @{thm ex1_implies_ex} RS exE] @
maps (mk_funs_inv thy5 o #1) newT_iso_axms) 1),
TRY (hyp_subst_tac ctxt 1),
rtac (sym RS range_eqI) 1,
@@ -559,10 +559,10 @@
(fn {context = ctxt, ...} => EVERY
[rtac iffI 1,
REPEAT (etac conjE 2), hyp_subst_tac ctxt 2, rtac refl 2,
- dresolve_tac rep_congs 1, dtac box_equals 1,
+ dresolve_tac rep_congs 1, dtac @{thm box_equals} 1,
REPEAT (resolve_tac rep_thms 1),
REPEAT (eresolve_tac inj_thms 1),
- REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac ext 1),
+ REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac @{thm ext} 1),
REPEAT (eresolve_tac (make_elim fun_cong :: inj_thms) 1),
atac 1]))])
end;
--- a/src/HOL/Tools/Datatype/rep_datatype.ML Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML Fri Mar 07 22:30:58 2014 +0100
@@ -172,7 +172,7 @@
in
(EVERY
[DETERM tac,
- REPEAT (etac ex1E 1), rtac ex1I 1,
+ REPEAT (etac @{thm ex1E} 1), rtac @{thm ex1I} 1,
DEPTH_SOLVE_1 (ares_tac [intr] 1),
REPEAT_DETERM_N k (etac thin_rl 1 THEN rotate_tac 1 1),
etac elim 1,
--- a/src/HOL/Tools/Function/function_core.ML Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/Function/function_core.ML Fri Mar 07 22:30:58 2014 +0100
@@ -366,7 +366,7 @@
val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
val exactly_one =
- ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
+ @{thm ex1I} |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
|> curry (op COMP) existence
|> curry (op COMP) uniqueness
|> simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp RS sym])
--- a/src/HOL/Tools/Meson/meson.ML Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/Meson/meson.ML Fri Mar 07 22:30:58 2014 +0100
@@ -707,7 +707,7 @@
fun MESON preskolem_tac mkcl cltac ctxt i st =
SELECT_GOAL
(EVERY [Object_Logic.atomize_prems_tac ctxt 1,
- rtac ccontr 1,
+ rtac @{thm ccontr} 1,
preskolem_tac,
Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
EVERY1 [skolemize_prems_tac ctxt negs,
--- a/src/HOL/Tools/inductive_set.ML Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/inductive_set.ML Fri Mar 07 22:30:58 2014 +0100
@@ -106,7 +106,7 @@
SOME (close (Goal.prove ctxt [] [])
(Logic.mk_equals (t, fold_rev Term.abs xs (m $ p $ (bop $ S $ S'))))
(K (EVERY
- [rtac eq_reflection 1, REPEAT (rtac ext 1), rtac iffI 1,
+ [rtac eq_reflection 1, REPEAT (rtac @{thm ext} 1), rtac iffI 1,
EVERY [etac conjE 1, rtac IntI 1, simp, simp,
etac IntE 1, rtac conjI 1, simp, simp] ORELSE
EVERY [etac disjE 1, rtac UnI1 1, simp, rtac UnI2 1, simp,
@@ -527,7 +527,7 @@
fold_rev (Term.abs o pair "x") Ts
(HOLogic.mk_mem (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)),
list_comb (c, params))))))
- (K (REPEAT (rtac ext 1) THEN simp_tac (put_simpset HOL_basic_ss lthy addsimps
+ (K (REPEAT (rtac @{thm ext} 1) THEN simp_tac (put_simpset HOL_basic_ss lthy addsimps
[def, mem_Collect_eq, @{thm split_conv}]) 1))
in
lthy |> Local_Theory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
--- a/src/HOL/Tools/lin_arith.ML Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/lin_arith.ML Fri Mar 07 22:30:58 2014 +0100
@@ -33,7 +33,7 @@
structure LA_Logic: LIN_ARITH_LOGIC =
struct
-val ccontr = ccontr;
+val ccontr = @{thm ccontr};
val conjI = conjI;
val notI = notI;
val sym = sym;
@@ -733,7 +733,7 @@
EVERY' [
REPEAT_DETERM o etac rev_mp,
cond_split_tac,
- rtac ccontr,
+ rtac @{thm ccontr},
prem_nnf_tac ctxt,
TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac [conjE, exE] ORELSE' etac disjE))
]
--- a/src/HOL/Tools/sat.ML Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/sat.ML Fri Mar 07 22:30:58 2014 +0100
@@ -419,7 +419,7 @@
(* ------------------------------------------------------------------------- *)
fun pre_cnf_tac ctxt =
- rtac ccontr THEN'
+ rtac @{thm ccontr} THEN'
Object_Logic.atomize_prems_tac ctxt THEN'
CONVERSION Drule.beta_eta_conversion;