--- a/src/HOL/Bali/AxExample.thy Wed May 26 21:20:18 2010 +0200
+++ b/src/HOL/Bali/AxExample.thy Thu May 27 08:02:02 2010 +0200
@@ -189,7 +189,7 @@
apply (tactic "ax_tac 1")
apply (rule_tac [2] ax_subst_Var_allI)
apply (tactic {* inst1_tac @{context} "P'" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})
-apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [split_paired_All, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2 *})
+apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [@{thm split_paired_All}, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2 *})
apply (tactic "ax_tac 2" (* NewA *))
apply (tactic "ax_tac 3" (* ax_Alloc_Arr *))
apply (tactic "ax_tac 3")
--- a/src/HOL/Hoare/hoare_tac.ML Wed May 26 21:20:18 2010 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML Thu May 27 08:02:02 2010 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Hoare/hoare_tac.ML
- ID: $Id$
Author: Leonor Prensa Nieto & Tobias Nipkow
Derivation of the proof rules and, most importantly, the VCG tactic.
@@ -17,8 +16,8 @@
local open HOLogic in
(** maps (%x1 ... xn. t) to [x1,...,xn] **)
-fun abs2list (Const ("split",_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
- | abs2list (Abs(x,T,t)) = [Free (x, T)]
+fun abs2list (Const (@{const_name split}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
+ | abs2list (Abs (x, T, t)) = [Free (x, T)]
| abs2list _ = [];
(** maps {(x1,...,xn). t} to [x1,...,xn] **)
@@ -33,7 +32,7 @@
else let val z = mk_abstupleC w body;
val T2 = case z of Abs(_,T,_) => T
| Const (_, Type (_,[_, Type (_,[T,_])])) $ _ => T;
- in Const ("split", (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT)
+ in Const (@{const_name split}, (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT)
$ absfree (n, T, z) end end;
(** maps [x1,...,xn] to (x1,...,xn) and types**)
@@ -91,7 +90,7 @@
val before_set2pred_simp_tac =
(simp_tac (HOL_basic_ss addsimps [Collect_conj_eq RS sym, @{thm Compl_Collect}]));
-val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split_conv]));
+val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [@{thm split_conv}]));
(*****************************************************************************)
(** set2pred_tac transforms sets inclusion into predicates implication, **)
@@ -112,7 +111,7 @@
rtac CollectI i,
dtac CollectD i,
TRY (split_all_tac i) THEN_MAYBE
- (rename_tac var_names i THEN full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)]);
+ (rename_tac var_names i THEN full_simp_tac (HOL_basic_ss addsimps [@{thm split_conv}]) i)]);
(*****************************************************************************)
(** BasicSimpTac is called to simplify all verification conditions. It does **)
@@ -126,7 +125,7 @@
fun BasicSimpTac var_names tac =
simp_tac
- (HOL_basic_ss addsimps [mem_Collect_eq, split_conv] addsimprocs [record_simproc])
+ (HOL_basic_ss addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [record_simproc])
THEN_MAYBE' MaxSimpTac var_names tac;
--- a/src/HOL/Hoare_Parallel/OG_Tactics.thy Wed May 26 21:20:18 2010 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Tactics.thy Thu May 27 08:02:02 2010 +0200
@@ -275,7 +275,7 @@
ML {*
val before_interfree_simp_tac = (simp_tac (HOL_basic_ss addsimps [thm "com.simps", thm "post.simps"]))
-val interfree_simp_tac = (asm_simp_tac (HOL_ss addsimps [thm "split", thm "ball_Un", thm "ball_empty"]@(thms "my_simp_list")))
+val interfree_simp_tac = (asm_simp_tac (HOL_ss addsimps [@{thm split}, thm "ball_Un", thm "ball_empty"]@(thms "my_simp_list")))
val ParallelConseq = (simp_tac (HOL_basic_ss addsimps (thms "ParallelConseq_list")@(thms "my_simp_list")))
*}
--- a/src/HOL/MicroJava/J/Conform.thy Wed May 26 21:20:18 2010 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy Thu May 27 08:02:02 2010 +0200
@@ -328,8 +328,8 @@
apply auto
apply(rule hconfI)
apply(drule conforms_heapD)
-apply(tactic {* auto_tac (HOL_cs addEs [thm "oconf_hext"]
- addDs [thm "hconfD"], @{simpset} delsimps [split_paired_All]) *})
+apply(tactic {* auto_tac (HOL_cs addEs [@{thm oconf_hext}]
+ addDs [@{thm hconfD}], @{simpset} delsimps [@{thm split_paired_All}]) *})
done
lemma conforms_upd_local:
--- a/src/HOL/Modelcheck/MuckeSyn.thy Wed May 26 21:20:18 2010 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.thy Thu May 27 08:02:02 2010 +0200
@@ -228,7 +228,7 @@
EVERY [
REPEAT (etac thin_rl i),
cut_facts_tac (mk_lam_defs defs) i,
- full_simp_tac (Mucke_ss delsimps [not_iff,split_part]) i,
+ full_simp_tac (Mucke_ss delsimps [not_iff, @{thm split_part}]) i,
move_mus i, call_mucke_tac i,atac i,
REPEAT (rtac refl i)] state);
*}
--- a/src/HOL/Modelcheck/mucke_oracle.ML Wed May 26 21:20:18 2010 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Thu May 27 08:02:02 2010 +0200
@@ -323,7 +323,7 @@
let val VarAbs = Syntax.variant_abs(s,tp,trm);
in get_decls sign (Const(fst VarAbs,tp)::Clist) (snd VarAbs)
end
- | get_decls sign Clist ((Const("split",_)) $ trm) = get_decls sign Clist trm
+ | get_decls sign Clist ((Const (@{const_name split}, _)) $ trm) = get_decls sign Clist trm
| get_decls sign Clist trm = (Clist,trm);
fun make_mu_def sign ((tt $ LHS) $ (ttt $ RHS)) =
@@ -389,9 +389,9 @@
val t2 = t1 $ ParamDeclTerm
in t2 end;
-fun is_fundef (( Const("==",_) $ _) $ ((Const("split",_)) $ _)) = true |
-is_fundef (( Const("==",_) $ _) $ Abs(x_T_t)) = true
-| is_fundef _ = false;
+fun is_fundef (Const("==", _) $ _ $ (Const (@{const_name split}, _) $ _)) = true
+ | is_fundef (Const("==", _) $ _ $ Abs _) = true
+ | is_fundef _ = false;
fun make_mucke_fun_def sign ((_ $ LHS) $ RHS) =
let (* fun dest_atom (Const t) = dest_Const (Const t)
--- a/src/HOL/Nominal/nominal_induct.ML Wed May 26 21:20:18 2010 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML Thu May 27 08:02:02 2010 +0200
@@ -23,7 +23,7 @@
val split_all_tuples =
Simplifier.full_simplify (HOL_basic_ss addsimps
- [split_conv, split_paired_all, unit_all_eq1, @{thm fresh_unit_elim}, @{thm fresh_prod_elim}] @
+ [@{thm split_conv}, @{thm split_paired_all}, @{thm unit_all_eq1}, @{thm fresh_unit_elim}, @{thm fresh_prod_elim}] @
@{thms fresh_star_unit_elim} @ @{thms fresh_star_prod_elim});
--- a/src/HOL/Product_Type.thy Wed May 26 21:20:18 2010 +0200
+++ b/src/HOL/Product_Type.thy Thu May 27 08:02:02 2010 +0200
@@ -1147,101 +1147,6 @@
end
*}
-
-subsection {* Legacy bindings *}
-
-ML {*
-val Collect_split = thm "Collect_split";
-val Compl_Times_UNIV1 = thm "Compl_Times_UNIV1";
-val Compl_Times_UNIV2 = thm "Compl_Times_UNIV2";
-val PairE = thm "PairE";
-val Pair_Rep_inject = thm "Pair_Rep_inject";
-val Pair_def = thm "Pair_def";
-val Pair_eq = @{thm "prod.inject"};
-val Pair_fst_snd_eq = thm "Pair_fst_snd_eq";
-val ProdI = thm "ProdI";
-val SetCompr_Sigma_eq = thm "SetCompr_Sigma_eq";
-val SigmaD1 = thm "SigmaD1";
-val SigmaD2 = thm "SigmaD2";
-val SigmaE = thm "SigmaE";
-val SigmaE2 = thm "SigmaE2";
-val SigmaI = thm "SigmaI";
-val Sigma_Diff_distrib1 = thm "Sigma_Diff_distrib1";
-val Sigma_Diff_distrib2 = thm "Sigma_Diff_distrib2";
-val Sigma_Int_distrib1 = thm "Sigma_Int_distrib1";
-val Sigma_Int_distrib2 = thm "Sigma_Int_distrib2";
-val Sigma_Un_distrib1 = thm "Sigma_Un_distrib1";
-val Sigma_Un_distrib2 = thm "Sigma_Un_distrib2";
-val Sigma_Union = thm "Sigma_Union";
-val Sigma_def = thm "Sigma_def";
-val Sigma_empty1 = thm "Sigma_empty1";
-val Sigma_empty2 = thm "Sigma_empty2";
-val Sigma_mono = thm "Sigma_mono";
-val The_split = thm "The_split";
-val The_split_eq = thm "The_split_eq";
-val The_split_eq = thm "The_split_eq";
-val Times_Diff_distrib1 = thm "Times_Diff_distrib1";
-val Times_Int_distrib1 = thm "Times_Int_distrib1";
-val Times_Un_distrib1 = thm "Times_Un_distrib1";
-val Times_eq_cancel2 = thm "Times_eq_cancel2";
-val Times_subset_cancel2 = thm "Times_subset_cancel2";
-val UNIV_Times_UNIV = thm "UNIV_Times_UNIV";
-val UN_Times_distrib = thm "UN_Times_distrib";
-val Unity_def = thm "Unity_def";
-val cond_split_eta = thm "cond_split_eta";
-val fst_conv = thm "fst_conv";
-val fst_def = thm "fst_def";
-val fst_eqD = thm "fst_eqD";
-val inj_on_Abs_Prod = thm "inj_on_Abs_Prod";
-val mem_Sigma_iff = thm "mem_Sigma_iff";
-val mem_splitE = thm "mem_splitE";
-val mem_splitI = thm "mem_splitI";
-val mem_splitI2 = thm "mem_splitI2";
-val prod_eqI = thm "prod_eqI";
-val prod_fun = thm "prod_fun";
-val prod_fun_compose = thm "prod_fun_compose";
-val prod_fun_def = thm "prod_fun_def";
-val prod_fun_ident = thm "prod_fun_ident";
-val prod_fun_imageE = thm "prod_fun_imageE";
-val prod_fun_imageI = thm "prod_fun_imageI";
-val prod_induct = thm "prod.induct";
-val snd_conv = thm "snd_conv";
-val snd_def = thm "snd_def";
-val snd_eqD = thm "snd_eqD";
-val split = thm "split";
-val splitD = thm "splitD";
-val splitD' = thm "splitD'";
-val splitE = thm "splitE";
-val splitE' = thm "splitE'";
-val splitE2 = thm "splitE2";
-val splitI = thm "splitI";
-val splitI2 = thm "splitI2";
-val splitI2' = thm "splitI2'";
-val split_beta = thm "split_beta";
-val split_conv = thm "split_conv";
-val split_def = thm "split_def";
-val split_eta = thm "split_eta";
-val split_eta_SetCompr = thm "split_eta_SetCompr";
-val split_eta_SetCompr2 = thm "split_eta_SetCompr2";
-val split_paired_All = thm "split_paired_All";
-val split_paired_Ball_Sigma = thm "split_paired_Ball_Sigma";
-val split_paired_Bex_Sigma = thm "split_paired_Bex_Sigma";
-val split_paired_Ex = thm "split_paired_Ex";
-val split_paired_The = thm "split_paired_The";
-val split_paired_all = thm "split_paired_all";
-val split_part = thm "split_part";
-val split_split = thm "split_split";
-val split_split_asm = thm "split_split_asm";
-val split_tupled_all = thms "split_tupled_all";
-val split_weak_cong = thm "split_weak_cong";
-val surj_pair = thm "surj_pair";
-val surjective_pairing = thm "surjective_pairing";
-val unit_abs_eta_conv = thm "unit_abs_eta_conv";
-val unit_all_eq1 = thm "unit_all_eq1";
-val unit_all_eq2 = thm "unit_all_eq2";
-val unit_eq = thm "unit_eq";
-*}
-
use "Tools/inductive_set.ML"
setup Inductive_Set.setup
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Wed May 26 21:20:18 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Thu May 27 08:02:02 2010 +0200
@@ -113,7 +113,7 @@
val thm = OldGoals.simple_prove_goal_cterm (cert (Logic.list_implies (prems, concl)))
(fn prems =>
- [rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
+ [rewrite_goals_tac (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
rtac (cterm_instantiate inst induct) 1,
ALLGOALS Object_Logic.atomize_prems_tac,
rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites),
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed May 26 21:20:18 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu May 27 08:02:02 2010 +0200
@@ -2015,7 +2015,7 @@
| split_lambda (Const ("Product_Type.Unity", _)) t = Abs ("x", HOLogic.unitT, t)
| split_lambda t _ = raise (TERM ("split_lambda", [t]))
-fun strip_split_abs (Const ("split", _) $ t) = strip_split_abs t
+fun strip_split_abs (Const (@{const_name split}, _) $ t) = strip_split_abs t
| strip_split_abs (Abs (_, _, t)) = strip_split_abs t
| strip_split_abs t = t
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed May 26 21:20:18 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu May 27 08:02:02 2010 +0200
@@ -179,7 +179,7 @@
|> maps (fn (res, (names, prems)) =>
flatten' (betapply (g, res)) (names, prems))
end)
- | Const (@{const_name "split"}, _) =>
+ | Const (@{const_name split}, _) =>
(let
val (_, g :: res :: args) = strip_comb t
val [res1, res2] = Name.variant_list names ["res1", "res2"]
--- a/src/HOL/Tools/Quotient/quotient_term.ML Wed May 26 21:20:18 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Thu May 27 08:02:02 2010 +0200
@@ -560,12 +560,12 @@
end
end
- | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
- ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) =>
+ | (((t1 as Const (@{const_name split}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
+ ((t2 as Const (@{const_name split}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) =>
regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
- | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, s1)),
- ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , s2))) =>
+ | (((t1 as Const (@{const_name split}, _)) $ Abs (v1, ty, s1)),
+ ((t2 as Const (@{const_name split}, _)) $ Abs (v2, _ , s2))) =>
regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2))
| (t1 $ t2, t1' $ t2') =>
--- a/src/HOL/Tools/TFL/rules.ML Wed May 26 21:20:18 2010 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Thu May 27 08:02:02 2010 +0200
@@ -623,7 +623,7 @@
val thm2 = forall_intr_list (map tych L) thm1
val thm3 = forall_elim_list (XFILL tych a vstr) thm2
in refl RS
- rewrite_rule [Thm.symmetric (surjective_pairing RS eq_reflection)] thm3
+ rewrite_rule [Thm.symmetric (@{thm surjective_pairing} RS eq_reflection)] thm3
end;
fun PGEN tych a vstr th =
@@ -663,7 +663,7 @@
fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
let val globals = func::G
val ss0 = Simplifier.global_context (Thm.theory_of_thm th) empty_ss
- val pbeta_reduce = simpl_conv ss0 [split_conv RS eq_reflection];
+ val pbeta_reduce = simpl_conv ss0 [@{thm split_conv} RS eq_reflection];
val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref
val dummy = term_ref := []
val dummy = thm_ref := []
--- a/src/HOL/Tools/TFL/usyntax.ML Wed May 26 21:20:18 2010 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML Thu May 27 08:02:02 2010 +0200
@@ -195,8 +195,8 @@
fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2);
local
-fun mk_uncurry(xt,yt,zt) =
- Const("split",(xt --> yt --> zt) --> prod_ty xt yt --> zt)
+fun mk_uncurry (xt, yt, zt) =
+ Const(@{const_name split}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
| dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
@@ -276,7 +276,7 @@
| dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
-local fun ucheck t = (if #Name(dest_const t) = "split" then t
+local fun ucheck t = (if #Name (dest_const t) = @{const_name split} then t
else raise Match)
in
fun dest_pabs used tm =
--- a/src/HOL/Tools/inductive_realizer.ML Wed May 26 21:20:18 2010 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Thu May 27 08:02:02 2010 +0200
@@ -389,7 +389,7 @@
end) (rlzs ~~ rnames);
val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
(fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
- val rews = map mk_meta_eq (fst_conv :: snd_conv :: rec_thms);
+ val rews = map mk_meta_eq (@{thm fst_conv} :: @{thm snd_conv} :: rec_thms);
val thm = Goal.prove_global thy [] prems concl (fn {prems, ...} => EVERY
[rtac (#raw_induct ind_info) 1,
rewrite_goals_tac rews,
--- a/src/HOL/Tools/inductive_set.ML Wed May 26 21:20:18 2010 +0200
+++ b/src/HOL/Tools/inductive_set.ML Thu May 27 08:02:02 2010 +0200
@@ -44,7 +44,7 @@
ts = map Bound (length ps downto 0)
then
let val simp = full_simp_tac (Simplifier.inherit_context ss
- (HOL_basic_ss addsimps [split_paired_all, split_conv])) 1
+ (HOL_basic_ss addsimps [@{thm split_paired_all}, @{thm split_conv}])) 1
in
SOME (Goal.prove (Simplifier.the_context ss) [] []
(Const ("==", T --> T --> propT) $ S $ S')
@@ -92,7 +92,7 @@
mkop s T (m, p, mk_collect p T (head_of u), S)
| decomp _ = NONE;
val simp = full_simp_tac (Simplifier.inherit_context ss
- (HOL_basic_ss addsimps [mem_Collect_eq, split_conv])) 1;
+ (HOL_basic_ss addsimps [mem_Collect_eq, @{thm split_conv}])) 1;
fun mk_rew t = (case strip_abs_vars t of
[] => NONE
| xs => (case decomp (strip_abs_body t) of
@@ -255,7 +255,7 @@
HOLogic.boolT (Bound 0))))] arg_cong' RS sym)
end)
in
- Simplifier.simplify (HOL_basic_ss addsimps [mem_Collect_eq, split_conv]
+ Simplifier.simplify (HOL_basic_ss addsimps [mem_Collect_eq, @{thm split_conv}]
addsimprocs [collect_mem_simproc]) thm'' |>
zero_var_indexes |> eta_contract_thm (equal p)
end;
@@ -343,7 +343,7 @@
thm |>
Thm.instantiate ([], insts) |>
Simplifier.full_simplify (HOL_basic_ss addsimprocs
- [to_pred_simproc (mem_Collect_eq :: split_conv :: to_pred_simps)]) |>
+ [to_pred_simproc (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps)]) |>
eta_contract_thm (is_pred pred_arities) |>
Rule_Cases.save thm
end;
@@ -396,7 +396,7 @@
then
thm |>
Simplifier.full_simplify (HOL_basic_ss addsimprocs
- [to_pred_simproc (mem_Collect_eq :: split_conv :: to_pred_simps)]) |>
+ [to_pred_simproc (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps)]) |>
eta_contract_thm (is_pred pred_arities)
else thm
in map preproc end;
@@ -463,7 +463,7 @@
end) |> split_list |>> split_list;
val eqns' = eqns @
map (prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq)
- (mem_Collect_eq :: split_conv :: to_pred_simps);
+ (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps);
(* predicate version of the introduction rules *)
val intros' =
@@ -505,7 +505,7 @@
(HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)),
list_comb (c, params))))))
(K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
- [def, mem_Collect_eq, split_conv]) 1))
+ [def, mem_Collect_eq, @{thm split_conv}]) 1))
in
lthy |> Local_Theory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
[Attrib.internal (K pred_set_conv_att)]),
--- a/src/HOL/Tools/quickcheck_generators.ML Wed May 26 21:20:18 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Thu May 27 08:02:02 2010 +0200
@@ -188,7 +188,7 @@
fun tac { context = ctxt, prems = _ } =
ALLGOALS (simp_tac (HOL_ss addsimps proj_simps))
THEN ALLGOALS (EqSubst.eqsubst_tac ctxt [0] [aux_simp])
- THEN ALLGOALS (simp_tac (HOL_ss addsimps [fst_conv, snd_conv]));
+ THEN ALLGOALS (simp_tac (HOL_ss addsimps [@{thm fst_conv}, @{thm snd_conv}]));
in (map (fn prop => Skip_Proof.prove lthy [v] [] prop tac) eqs, lthy) end;
in
lthy
--- a/src/HOL/Tools/record.ML Wed May 26 21:20:18 2010 +0200
+++ b/src/HOL/Tools/record.ML Thu May 27 08:02:02 2010 +0200
@@ -2215,7 +2215,7 @@
prove_standard [] cases_prop
(fn _ =>
try_param_tac rN cases_scheme 1 THEN
- simp_all_tac HOL_basic_ss [unit_all_eq1]);
+ simp_all_tac HOL_basic_ss [@{thm unit_all_eq1}]);
val cases = timeit_msg "record cases proof:" cases_prf;
fun surjective_prf () =
--- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy Wed May 26 21:20:18 2010 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy Thu May 27 08:02:02 2010 +0200
@@ -276,13 +276,13 @@
OldGoals.by (REPEAT (dtac eq_reflection 1));
(* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *)
OldGoals.by (full_simp_tac ((global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs)
- delsimps [not_iff,split_part])
+ delsimps [not_iff, @{thm split_part}])
addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @
rename_simps @ ioa_simps @ asig_simps)) 1);
OldGoals.by (full_simp_tac
- (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1);
+ (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff, @{thm split_part}]) 1);
OldGoals.by (REPEAT (if_full_simp_tac
- (global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1));
+ (global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff, @{thm split_part}]) 1));
OldGoals.by (call_mucke_tac 1);
(* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *)
OldGoals.by (atac 1);
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Wed May 26 21:20:18 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Thu May 27 08:02:02 2010 +0200
@@ -1101,7 +1101,7 @@
THEN (REPEAT_DETERM (CHANGED (asm_simp_tac (simpset_of ctxt) i)));
fun pair_tac ctxt s =
- res_inst_tac ctxt [(("p", 0), s)] PairE
+ res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}
THEN' hyp_subst_tac THEN' asm_full_simp_tac (simpset_of ctxt);
(* induction on a sequence of pairs with pairsplitting and simplification *)