# HG changeset patch # User haftmann # Date 1274882725 -7200 # Node ID e0c9d3e49e15bc1dd34a336b6b06bedf9e13ea85 # Parent 636e6d8645d6fac17ce24c544e1839a612c70394 dropped legacy theorem bindings diff -r 636e6d8645d6 -r e0c9d3e49e15 src/HOL/Hoare_Parallel/OG_Tactics.thy --- a/src/HOL/Hoare_Parallel/OG_Tactics.thy Wed May 26 16:05:25 2010 +0200 +++ b/src/HOL/Hoare_Parallel/OG_Tactics.thy Wed May 26 16:05:25 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 636e6d8645d6 -r e0c9d3e49e15 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Wed May 26 16:05:25 2010 +0200 +++ b/src/HOL/Product_Type.thy Wed May 26 16:05:25 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 636e6d8645d6 -r e0c9d3e49e15 src/HOL/Tools/Datatype/datatype_realizer.ML --- a/src/HOL/Tools/Datatype/datatype_realizer.ML Wed May 26 16:05:25 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Wed May 26 16:05:25 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 636e6d8645d6 -r e0c9d3e49e15 src/HOL/Tools/TFL/rules.ML --- a/src/HOL/Tools/TFL/rules.ML Wed May 26 16:05:25 2010 +0200 +++ b/src/HOL/Tools/TFL/rules.ML Wed May 26 16:05:25 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 636e6d8645d6 -r e0c9d3e49e15 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Wed May 26 16:05:25 2010 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Wed May 26 16:05:25 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 636e6d8645d6 -r e0c9d3e49e15 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Wed May 26 16:05:25 2010 +0200 +++ b/src/HOL/Tools/inductive_set.ML Wed May 26 16:05:25 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 636e6d8645d6 -r e0c9d3e49e15 src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Wed May 26 16:05:25 2010 +0200 +++ b/src/HOL/Tools/quickcheck_generators.ML Wed May 26 16:05:25 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 636e6d8645d6 -r e0c9d3e49e15 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Wed May 26 16:05:25 2010 +0200 +++ b/src/HOL/Tools/record.ML Wed May 26 16:05:25 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 () =