# HG changeset patch # User haftmann # Date 1274940122 -7200 # Node ID 8d231d3efcde7e0bdfe2c1d4f303bee8e9278acb # Parent 29bd6c2ffba859520a2ff12bb6440246c9021f41# Parent 6ba1b0ef0cc48f0ad06be24f3514287255f3f493 merged diff -r 29bd6c2ffba8 -r 8d231d3efcde src/HOL/Bali/AxExample.thy --- 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'" "\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") diff -r 29bd6c2ffba8 -r 8d231d3efcde src/HOL/Hoare/hoare_tac.ML --- 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; diff -r 29bd6c2ffba8 -r 8d231d3efcde src/HOL/Hoare_Parallel/OG_Tactics.thy --- 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"))) *} diff -r 29bd6c2ffba8 -r 8d231d3efcde src/HOL/MicroJava/J/Conform.thy --- 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: diff -r 29bd6c2ffba8 -r 8d231d3efcde src/HOL/Modelcheck/MuckeSyn.thy --- 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); *} diff -r 29bd6c2ffba8 -r 8d231d3efcde src/HOL/Modelcheck/mucke_oracle.ML --- 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) diff -r 29bd6c2ffba8 -r 8d231d3efcde src/HOL/Nominal/nominal_induct.ML --- 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}); diff -r 29bd6c2ffba8 -r 8d231d3efcde src/HOL/Product_Type.thy --- 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 diff -r 29bd6c2ffba8 -r 8d231d3efcde src/HOL/Tools/Datatype/datatype_realizer.ML --- 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), diff -r 29bd6c2ffba8 -r 8d231d3efcde src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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 diff -r 29bd6c2ffba8 -r 8d231d3efcde src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- 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"] diff -r 29bd6c2ffba8 -r 8d231d3efcde src/HOL/Tools/Quotient/quotient_term.ML --- 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') => diff -r 29bd6c2ffba8 -r 8d231d3efcde src/HOL/Tools/TFL/rules.ML --- 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 := [] diff -r 29bd6c2ffba8 -r 8d231d3efcde src/HOL/Tools/TFL/usyntax.ML --- 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 = diff -r 29bd6c2ffba8 -r 8d231d3efcde src/HOL/Tools/inductive_realizer.ML --- 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, diff -r 29bd6c2ffba8 -r 8d231d3efcde src/HOL/Tools/inductive_set.ML --- 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)]), diff -r 29bd6c2ffba8 -r 8d231d3efcde src/HOL/Tools/quickcheck_generators.ML --- 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 diff -r 29bd6c2ffba8 -r 8d231d3efcde src/HOL/Tools/record.ML --- 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 () = diff -r 29bd6c2ffba8 -r 8d231d3efcde src/HOLCF/IOA/Modelcheck/MuIOA.thy --- 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); diff -r 29bd6c2ffba8 -r 8d231d3efcde src/HOLCF/IOA/meta_theory/Sequence.thy --- 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 *)