merged
authorhaftmann
Thu May 27 08:02:02 2010 +0200 (2010-05-27)
changeset 371418d231d3efcde
parent 37134 29bd6c2ffba8
parent 37140 6ba1b0ef0cc4
child 37142 56e1b6976d0e
merged
     1.1 --- a/src/HOL/Bali/AxExample.thy	Wed May 26 21:20:18 2010 +0200
     1.2 +++ b/src/HOL/Bali/AxExample.thy	Thu May 27 08:02:02 2010 +0200
     1.3 @@ -189,7 +189,7 @@
     1.4  apply     (tactic "ax_tac 1")
     1.5  apply     (rule_tac [2] ax_subst_Var_allI)
     1.6  apply      (tactic {* inst1_tac @{context} "P'" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})
     1.7 -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 *})
     1.8 +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 *})
     1.9  apply      (tactic "ax_tac 2" (* NewA *))
    1.10  apply       (tactic "ax_tac 3" (* ax_Alloc_Arr *))
    1.11  apply       (tactic "ax_tac 3")
     2.1 --- a/src/HOL/Hoare/hoare_tac.ML	Wed May 26 21:20:18 2010 +0200
     2.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Thu May 27 08:02:02 2010 +0200
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title:      HOL/Hoare/hoare_tac.ML
     2.5 -    ID:         $Id$
     2.6      Author:     Leonor Prensa Nieto & Tobias Nipkow
     2.7  
     2.8  Derivation of the proof rules and, most importantly, the VCG tactic.
     2.9 @@ -17,8 +16,8 @@
    2.10  local open HOLogic in
    2.11  
    2.12  (** maps (%x1 ... xn. t) to [x1,...,xn] **)
    2.13 -fun abs2list (Const ("split",_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
    2.14 -  | abs2list (Abs(x,T,t)) = [Free (x, T)]
    2.15 +fun abs2list (Const (@{const_name split}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
    2.16 +  | abs2list (Abs (x, T, t)) = [Free (x, T)]
    2.17    | abs2list _ = [];
    2.18  
    2.19  (** maps {(x1,...,xn). t} to [x1,...,xn] **)
    2.20 @@ -33,7 +32,7 @@
    2.21          else let val z  = mk_abstupleC w body;
    2.22                   val T2 = case z of Abs(_,T,_) => T
    2.23                          | Const (_, Type (_,[_, Type (_,[T,_])])) $ _ => T;
    2.24 -       in Const ("split", (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT)
    2.25 +       in Const (@{const_name split}, (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT)
    2.26            $ absfree (n, T, z) end end;
    2.27  
    2.28  (** maps [x1,...,xn] to (x1,...,xn) and types**)
    2.29 @@ -91,7 +90,7 @@
    2.30  val before_set2pred_simp_tac =
    2.31    (simp_tac (HOL_basic_ss addsimps [Collect_conj_eq RS sym, @{thm Compl_Collect}]));
    2.32  
    2.33 -val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split_conv]));
    2.34 +val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [@{thm split_conv}]));
    2.35  
    2.36  (*****************************************************************************)
    2.37  (** set2pred_tac transforms sets inclusion into predicates implication,     **)
    2.38 @@ -112,7 +111,7 @@
    2.39      rtac CollectI i,
    2.40      dtac CollectD i,
    2.41      TRY (split_all_tac i) THEN_MAYBE
    2.42 -     (rename_tac var_names i THEN full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)]);
    2.43 +     (rename_tac var_names i THEN full_simp_tac (HOL_basic_ss addsimps [@{thm split_conv}]) i)]);
    2.44  
    2.45  (*****************************************************************************)
    2.46  (** BasicSimpTac is called to simplify all verification conditions. It does **)
    2.47 @@ -126,7 +125,7 @@
    2.48  
    2.49  fun BasicSimpTac var_names tac =
    2.50    simp_tac
    2.51 -    (HOL_basic_ss addsimps [mem_Collect_eq, split_conv] addsimprocs [record_simproc])
    2.52 +    (HOL_basic_ss addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [record_simproc])
    2.53    THEN_MAYBE' MaxSimpTac var_names tac;
    2.54  
    2.55  
     3.1 --- a/src/HOL/Hoare_Parallel/OG_Tactics.thy	Wed May 26 21:20:18 2010 +0200
     3.2 +++ b/src/HOL/Hoare_Parallel/OG_Tactics.thy	Thu May 27 08:02:02 2010 +0200
     3.3 @@ -275,7 +275,7 @@
     3.4  ML {*
     3.5  val before_interfree_simp_tac = (simp_tac (HOL_basic_ss addsimps [thm "com.simps", thm "post.simps"]))
     3.6  
     3.7 -val  interfree_simp_tac = (asm_simp_tac (HOL_ss addsimps [thm "split", thm "ball_Un", thm "ball_empty"]@(thms "my_simp_list")))
     3.8 +val  interfree_simp_tac = (asm_simp_tac (HOL_ss addsimps [@{thm split}, thm "ball_Un", thm "ball_empty"]@(thms "my_simp_list")))
     3.9  
    3.10  val ParallelConseq = (simp_tac (HOL_basic_ss addsimps (thms "ParallelConseq_list")@(thms "my_simp_list")))
    3.11  *}
     4.1 --- a/src/HOL/MicroJava/J/Conform.thy	Wed May 26 21:20:18 2010 +0200
     4.2 +++ b/src/HOL/MicroJava/J/Conform.thy	Thu May 27 08:02:02 2010 +0200
     4.3 @@ -328,8 +328,8 @@
     4.4  apply  auto
     4.5  apply(rule hconfI)
     4.6  apply(drule conforms_heapD)
     4.7 -apply(tactic {* auto_tac (HOL_cs addEs [thm "oconf_hext"] 
     4.8 -                addDs [thm "hconfD"], @{simpset} delsimps [split_paired_All]) *})
     4.9 +apply(tactic {* auto_tac (HOL_cs addEs [@{thm oconf_hext}] 
    4.10 +                addDs [@{thm hconfD}], @{simpset} delsimps [@{thm split_paired_All}]) *})
    4.11  done
    4.12  
    4.13  lemma conforms_upd_local: 
     5.1 --- a/src/HOL/Modelcheck/MuckeSyn.thy	Wed May 26 21:20:18 2010 +0200
     5.2 +++ b/src/HOL/Modelcheck/MuckeSyn.thy	Thu May 27 08:02:02 2010 +0200
     5.3 @@ -228,7 +228,7 @@
     5.4        EVERY [
     5.5          REPEAT (etac thin_rl i),
     5.6          cut_facts_tac (mk_lam_defs defs) i,
     5.7 -        full_simp_tac (Mucke_ss delsimps [not_iff,split_part]) i,
     5.8 +        full_simp_tac (Mucke_ss delsimps [not_iff, @{thm split_part}]) i,
     5.9          move_mus i, call_mucke_tac i,atac i,
    5.10          REPEAT (rtac refl i)] state);
    5.11  *}
     6.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Wed May 26 21:20:18 2010 +0200
     6.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Thu May 27 08:02:02 2010 +0200
     6.3 @@ -323,7 +323,7 @@
     6.4      let val VarAbs = Syntax.variant_abs(s,tp,trm);
     6.5      in get_decls sign (Const(fst VarAbs,tp)::Clist) (snd VarAbs)
     6.6      end
     6.7 -  | get_decls sign Clist ((Const("split",_)) $ trm) = get_decls sign Clist trm
     6.8 +  | get_decls sign Clist ((Const (@{const_name split}, _)) $ trm) = get_decls sign Clist trm
     6.9    | get_decls sign Clist trm = (Clist,trm);
    6.10  
    6.11  fun make_mu_def sign ((tt $ LHS) $ (ttt $ RHS)) =
    6.12 @@ -389,9 +389,9 @@
    6.13        val t2 = t1 $ ParamDeclTerm
    6.14    in t2 end;
    6.15  
    6.16 -fun is_fundef (( Const("==",_) $ _) $ ((Const("split",_)) $ _)) = true |
    6.17 -is_fundef (( Const("==",_) $ _) $ Abs(x_T_t)) = true 
    6.18 -| is_fundef _ = false; 
    6.19 +fun is_fundef (Const("==", _) $ _ $ (Const (@{const_name split}, _) $ _)) = true
    6.20 +  | is_fundef (Const("==", _) $ _ $ Abs _) = true 
    6.21 +  | is_fundef _ = false; 
    6.22  
    6.23  fun make_mucke_fun_def sign ((_ $ LHS) $ RHS) =
    6.24    let   (* fun dest_atom (Const t) = dest_Const (Const t)
     7.1 --- a/src/HOL/Nominal/nominal_induct.ML	Wed May 26 21:20:18 2010 +0200
     7.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Thu May 27 08:02:02 2010 +0200
     7.3 @@ -23,7 +23,7 @@
     7.4  
     7.5  val split_all_tuples =
     7.6    Simplifier.full_simplify (HOL_basic_ss addsimps
     7.7 -    [split_conv, split_paired_all, unit_all_eq1, @{thm fresh_unit_elim}, @{thm fresh_prod_elim}] @
     7.8 +    [@{thm split_conv}, @{thm split_paired_all}, @{thm unit_all_eq1}, @{thm fresh_unit_elim}, @{thm fresh_prod_elim}] @
     7.9      @{thms fresh_star_unit_elim} @ @{thms fresh_star_prod_elim});
    7.10  
    7.11  
     8.1 --- a/src/HOL/Product_Type.thy	Wed May 26 21:20:18 2010 +0200
     8.2 +++ b/src/HOL/Product_Type.thy	Thu May 27 08:02:02 2010 +0200
     8.3 @@ -1147,101 +1147,6 @@
     8.4  end
     8.5  *}
     8.6  
     8.7 -
     8.8 -subsection {* Legacy bindings *}
     8.9 -
    8.10 -ML {*
    8.11 -val Collect_split = thm "Collect_split";
    8.12 -val Compl_Times_UNIV1 = thm "Compl_Times_UNIV1";
    8.13 -val Compl_Times_UNIV2 = thm "Compl_Times_UNIV2";
    8.14 -val PairE = thm "PairE";
    8.15 -val Pair_Rep_inject = thm "Pair_Rep_inject";
    8.16 -val Pair_def = thm "Pair_def";
    8.17 -val Pair_eq = @{thm "prod.inject"};
    8.18 -val Pair_fst_snd_eq = thm "Pair_fst_snd_eq";
    8.19 -val ProdI = thm "ProdI";
    8.20 -val SetCompr_Sigma_eq = thm "SetCompr_Sigma_eq";
    8.21 -val SigmaD1 = thm "SigmaD1";
    8.22 -val SigmaD2 = thm "SigmaD2";
    8.23 -val SigmaE = thm "SigmaE";
    8.24 -val SigmaE2 = thm "SigmaE2";
    8.25 -val SigmaI = thm "SigmaI";
    8.26 -val Sigma_Diff_distrib1 = thm "Sigma_Diff_distrib1";
    8.27 -val Sigma_Diff_distrib2 = thm "Sigma_Diff_distrib2";
    8.28 -val Sigma_Int_distrib1 = thm "Sigma_Int_distrib1";
    8.29 -val Sigma_Int_distrib2 = thm "Sigma_Int_distrib2";
    8.30 -val Sigma_Un_distrib1 = thm "Sigma_Un_distrib1";
    8.31 -val Sigma_Un_distrib2 = thm "Sigma_Un_distrib2";
    8.32 -val Sigma_Union = thm "Sigma_Union";
    8.33 -val Sigma_def = thm "Sigma_def";
    8.34 -val Sigma_empty1 = thm "Sigma_empty1";
    8.35 -val Sigma_empty2 = thm "Sigma_empty2";
    8.36 -val Sigma_mono = thm "Sigma_mono";
    8.37 -val The_split = thm "The_split";
    8.38 -val The_split_eq = thm "The_split_eq";
    8.39 -val The_split_eq = thm "The_split_eq";
    8.40 -val Times_Diff_distrib1 = thm "Times_Diff_distrib1";
    8.41 -val Times_Int_distrib1 = thm "Times_Int_distrib1";
    8.42 -val Times_Un_distrib1 = thm "Times_Un_distrib1";
    8.43 -val Times_eq_cancel2 = thm "Times_eq_cancel2";
    8.44 -val Times_subset_cancel2 = thm "Times_subset_cancel2";
    8.45 -val UNIV_Times_UNIV = thm "UNIV_Times_UNIV";
    8.46 -val UN_Times_distrib = thm "UN_Times_distrib";
    8.47 -val Unity_def = thm "Unity_def";
    8.48 -val cond_split_eta = thm "cond_split_eta";
    8.49 -val fst_conv = thm "fst_conv";
    8.50 -val fst_def = thm "fst_def";
    8.51 -val fst_eqD = thm "fst_eqD";
    8.52 -val inj_on_Abs_Prod = thm "inj_on_Abs_Prod";
    8.53 -val mem_Sigma_iff = thm "mem_Sigma_iff";
    8.54 -val mem_splitE = thm "mem_splitE";
    8.55 -val mem_splitI = thm "mem_splitI";
    8.56 -val mem_splitI2 = thm "mem_splitI2";
    8.57 -val prod_eqI = thm "prod_eqI";
    8.58 -val prod_fun = thm "prod_fun";
    8.59 -val prod_fun_compose = thm "prod_fun_compose";
    8.60 -val prod_fun_def = thm "prod_fun_def";
    8.61 -val prod_fun_ident = thm "prod_fun_ident";
    8.62 -val prod_fun_imageE = thm "prod_fun_imageE";
    8.63 -val prod_fun_imageI = thm "prod_fun_imageI";
    8.64 -val prod_induct = thm "prod.induct";
    8.65 -val snd_conv = thm "snd_conv";
    8.66 -val snd_def = thm "snd_def";
    8.67 -val snd_eqD = thm "snd_eqD";
    8.68 -val split = thm "split";
    8.69 -val splitD = thm "splitD";
    8.70 -val splitD' = thm "splitD'";
    8.71 -val splitE = thm "splitE";
    8.72 -val splitE' = thm "splitE'";
    8.73 -val splitE2 = thm "splitE2";
    8.74 -val splitI = thm "splitI";
    8.75 -val splitI2 = thm "splitI2";
    8.76 -val splitI2' = thm "splitI2'";
    8.77 -val split_beta = thm "split_beta";
    8.78 -val split_conv = thm "split_conv";
    8.79 -val split_def = thm "split_def";
    8.80 -val split_eta = thm "split_eta";
    8.81 -val split_eta_SetCompr = thm "split_eta_SetCompr";
    8.82 -val split_eta_SetCompr2 = thm "split_eta_SetCompr2";
    8.83 -val split_paired_All = thm "split_paired_All";
    8.84 -val split_paired_Ball_Sigma = thm "split_paired_Ball_Sigma";
    8.85 -val split_paired_Bex_Sigma = thm "split_paired_Bex_Sigma";
    8.86 -val split_paired_Ex = thm "split_paired_Ex";
    8.87 -val split_paired_The = thm "split_paired_The";
    8.88 -val split_paired_all = thm "split_paired_all";
    8.89 -val split_part = thm "split_part";
    8.90 -val split_split = thm "split_split";
    8.91 -val split_split_asm = thm "split_split_asm";
    8.92 -val split_tupled_all = thms "split_tupled_all";
    8.93 -val split_weak_cong = thm "split_weak_cong";
    8.94 -val surj_pair = thm "surj_pair";
    8.95 -val surjective_pairing = thm "surjective_pairing";
    8.96 -val unit_abs_eta_conv = thm "unit_abs_eta_conv";
    8.97 -val unit_all_eq1 = thm "unit_all_eq1";
    8.98 -val unit_all_eq2 = thm "unit_all_eq2";
    8.99 -val unit_eq = thm "unit_eq";
   8.100 -*}
   8.101 -
   8.102  use "Tools/inductive_set.ML"
   8.103  setup Inductive_Set.setup
   8.104  
     9.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Wed May 26 21:20:18 2010 +0200
     9.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Thu May 27 08:02:02 2010 +0200
     9.3 @@ -113,7 +113,7 @@
     9.4  
     9.5      val thm = OldGoals.simple_prove_goal_cterm (cert (Logic.list_implies (prems, concl)))
     9.6        (fn prems =>
     9.7 -         [rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
     9.8 +         [rewrite_goals_tac (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
     9.9            rtac (cterm_instantiate inst induct) 1,
    9.10            ALLGOALS Object_Logic.atomize_prems_tac,
    9.11            rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites),
    10.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed May 26 21:20:18 2010 +0200
    10.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu May 27 08:02:02 2010 +0200
    10.3 @@ -2015,7 +2015,7 @@
    10.4    | split_lambda (Const ("Product_Type.Unity", _)) t = Abs ("x", HOLogic.unitT, t)
    10.5    | split_lambda t _ = raise (TERM ("split_lambda", [t]))
    10.6  
    10.7 -fun strip_split_abs (Const ("split", _) $ t) = strip_split_abs t
    10.8 +fun strip_split_abs (Const (@{const_name split}, _) $ t) = strip_split_abs t
    10.9    | strip_split_abs (Abs (_, _, t)) = strip_split_abs t
   10.10    | strip_split_abs t = t
   10.11  
    11.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed May 26 21:20:18 2010 +0200
    11.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu May 27 08:02:02 2010 +0200
    11.3 @@ -179,7 +179,7 @@
    11.4                |> maps (fn (res, (names, prems)) =>
    11.5                  flatten' (betapply (g, res)) (names, prems))
    11.6              end)
    11.7 -        | Const (@{const_name "split"}, _) => 
    11.8 +        | Const (@{const_name split}, _) => 
    11.9              (let
   11.10                val (_, g :: res :: args) = strip_comb t
   11.11                val [res1, res2] = Name.variant_list names ["res1", "res2"]
    12.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Wed May 26 21:20:18 2010 +0200
    12.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu May 27 08:02:02 2010 +0200
    12.3 @@ -560,12 +560,12 @@
    12.4             end
    12.5         end
    12.6  
    12.7 -  | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
    12.8 -     ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
    12.9 +  | (((t1 as Const (@{const_name split}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
   12.10 +     ((t2 as Const (@{const_name split}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
   12.11         regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
   12.12  
   12.13 -  | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, s1)),
   12.14 -     ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , s2))) =>
   12.15 +  | (((t1 as Const (@{const_name split}, _)) $ Abs (v1, ty, s1)),
   12.16 +     ((t2 as Const (@{const_name split}, _)) $ Abs (v2, _ , s2))) =>
   12.17         regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2))
   12.18  
   12.19    | (t1 $ t2, t1' $ t2') =>
    13.1 --- a/src/HOL/Tools/TFL/rules.ML	Wed May 26 21:20:18 2010 +0200
    13.2 +++ b/src/HOL/Tools/TFL/rules.ML	Thu May 27 08:02:02 2010 +0200
    13.3 @@ -623,7 +623,7 @@
    13.4        val thm2 = forall_intr_list (map tych L) thm1
    13.5        val thm3 = forall_elim_list (XFILL tych a vstr) thm2
    13.6    in refl RS
    13.7 -     rewrite_rule [Thm.symmetric (surjective_pairing RS eq_reflection)] thm3
    13.8 +     rewrite_rule [Thm.symmetric (@{thm surjective_pairing} RS eq_reflection)] thm3
    13.9    end;
   13.10  
   13.11  fun PGEN tych a vstr th =
   13.12 @@ -663,7 +663,7 @@
   13.13  fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
   13.14   let val globals = func::G
   13.15       val ss0 = Simplifier.global_context (Thm.theory_of_thm th) empty_ss
   13.16 -     val pbeta_reduce = simpl_conv ss0 [split_conv RS eq_reflection];
   13.17 +     val pbeta_reduce = simpl_conv ss0 [@{thm split_conv} RS eq_reflection];
   13.18       val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref
   13.19       val dummy = term_ref := []
   13.20       val dummy = thm_ref  := []
    14.1 --- a/src/HOL/Tools/TFL/usyntax.ML	Wed May 26 21:20:18 2010 +0200
    14.2 +++ b/src/HOL/Tools/TFL/usyntax.ML	Thu May 27 08:02:02 2010 +0200
    14.3 @@ -195,8 +195,8 @@
    14.4  fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2);
    14.5  
    14.6  local
    14.7 -fun mk_uncurry(xt,yt,zt) =
    14.8 -    Const("split",(xt --> yt --> zt) --> prod_ty xt yt --> zt)
    14.9 +fun mk_uncurry (xt, yt, zt) =
   14.10 +    Const(@{const_name split}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
   14.11  fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
   14.12    | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
   14.13  fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
   14.14 @@ -276,7 +276,7 @@
   14.15    | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
   14.16  
   14.17  
   14.18 -local  fun ucheck t = (if #Name(dest_const t) = "split" then t
   14.19 +local  fun ucheck t = (if #Name (dest_const t) = @{const_name split} then t
   14.20                         else raise Match)
   14.21  in
   14.22  fun dest_pabs used tm =
    15.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed May 26 21:20:18 2010 +0200
    15.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu May 27 08:02:02 2010 +0200
    15.3 @@ -389,7 +389,7 @@
    15.4            end) (rlzs ~~ rnames);
    15.5          val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
    15.6            (fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
    15.7 -        val rews = map mk_meta_eq (fst_conv :: snd_conv :: rec_thms);
    15.8 +        val rews = map mk_meta_eq (@{thm fst_conv} :: @{thm snd_conv} :: rec_thms);
    15.9          val thm = Goal.prove_global thy [] prems concl (fn {prems, ...} => EVERY
   15.10            [rtac (#raw_induct ind_info) 1,
   15.11             rewrite_goals_tac rews,
    16.1 --- a/src/HOL/Tools/inductive_set.ML	Wed May 26 21:20:18 2010 +0200
    16.2 +++ b/src/HOL/Tools/inductive_set.ML	Thu May 27 08:02:02 2010 +0200
    16.3 @@ -44,7 +44,7 @@
    16.4                      ts = map Bound (length ps downto 0)
    16.5                    then
    16.6                      let val simp = full_simp_tac (Simplifier.inherit_context ss
    16.7 -                      (HOL_basic_ss addsimps [split_paired_all, split_conv])) 1
    16.8 +                      (HOL_basic_ss addsimps [@{thm split_paired_all}, @{thm split_conv}])) 1
    16.9                      in
   16.10                        SOME (Goal.prove (Simplifier.the_context ss) [] []
   16.11                          (Const ("==", T --> T --> propT) $ S $ S')
   16.12 @@ -92,7 +92,7 @@
   16.13                mkop s T (m, p, mk_collect p T (head_of u), S)
   16.14          | decomp _ = NONE;
   16.15        val simp = full_simp_tac (Simplifier.inherit_context ss
   16.16 -        (HOL_basic_ss addsimps [mem_Collect_eq, split_conv])) 1;
   16.17 +        (HOL_basic_ss addsimps [mem_Collect_eq, @{thm split_conv}])) 1;
   16.18        fun mk_rew t = (case strip_abs_vars t of
   16.19            [] => NONE
   16.20          | xs => (case decomp (strip_abs_body t) of
   16.21 @@ -255,7 +255,7 @@
   16.22                    HOLogic.boolT (Bound 0))))] arg_cong' RS sym)
   16.23            end)
   16.24    in
   16.25 -    Simplifier.simplify (HOL_basic_ss addsimps [mem_Collect_eq, split_conv]
   16.26 +    Simplifier.simplify (HOL_basic_ss addsimps [mem_Collect_eq, @{thm split_conv}]
   16.27        addsimprocs [collect_mem_simproc]) thm'' |>
   16.28          zero_var_indexes |> eta_contract_thm (equal p)
   16.29    end;
   16.30 @@ -343,7 +343,7 @@
   16.31      thm |>
   16.32      Thm.instantiate ([], insts) |>
   16.33      Simplifier.full_simplify (HOL_basic_ss addsimprocs
   16.34 -      [to_pred_simproc (mem_Collect_eq :: split_conv :: to_pred_simps)]) |>
   16.35 +      [to_pred_simproc (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps)]) |>
   16.36      eta_contract_thm (is_pred pred_arities) |>
   16.37      Rule_Cases.save thm
   16.38    end;
   16.39 @@ -396,7 +396,7 @@
   16.40        then
   16.41          thm |>
   16.42          Simplifier.full_simplify (HOL_basic_ss addsimprocs
   16.43 -          [to_pred_simproc (mem_Collect_eq :: split_conv :: to_pred_simps)]) |>
   16.44 +          [to_pred_simproc (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps)]) |>
   16.45          eta_contract_thm (is_pred pred_arities)
   16.46        else thm
   16.47    in map preproc end;
   16.48 @@ -463,7 +463,7 @@
   16.49        end) |> split_list |>> split_list;
   16.50      val eqns' = eqns @
   16.51        map (prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq)
   16.52 -        (mem_Collect_eq :: split_conv :: to_pred_simps);
   16.53 +        (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps);
   16.54  
   16.55      (* predicate version of the introduction rules *)
   16.56      val intros' =
   16.57 @@ -505,7 +505,7 @@
   16.58                   (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)),
   16.59                    list_comb (c, params))))))
   16.60              (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
   16.61 -              [def, mem_Collect_eq, split_conv]) 1))
   16.62 +              [def, mem_Collect_eq, @{thm split_conv}]) 1))
   16.63          in
   16.64            lthy |> Local_Theory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
   16.65              [Attrib.internal (K pred_set_conv_att)]),
    17.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Wed May 26 21:20:18 2010 +0200
    17.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Thu May 27 08:02:02 2010 +0200
    17.3 @@ -188,7 +188,7 @@
    17.4              fun tac { context = ctxt, prems = _ } =
    17.5                ALLGOALS (simp_tac (HOL_ss addsimps proj_simps))
    17.6                THEN ALLGOALS (EqSubst.eqsubst_tac ctxt [0] [aux_simp])
    17.7 -              THEN ALLGOALS (simp_tac (HOL_ss addsimps [fst_conv, snd_conv]));
    17.8 +              THEN ALLGOALS (simp_tac (HOL_ss addsimps [@{thm fst_conv}, @{thm snd_conv}]));
    17.9            in (map (fn prop => Skip_Proof.prove lthy [v] [] prop tac) eqs, lthy) end;
   17.10        in
   17.11          lthy
    18.1 --- a/src/HOL/Tools/record.ML	Wed May 26 21:20:18 2010 +0200
    18.2 +++ b/src/HOL/Tools/record.ML	Thu May 27 08:02:02 2010 +0200
    18.3 @@ -2215,7 +2215,7 @@
    18.4        prove_standard [] cases_prop
    18.5          (fn _ =>
    18.6            try_param_tac rN cases_scheme 1 THEN
    18.7 -          simp_all_tac HOL_basic_ss [unit_all_eq1]);
    18.8 +          simp_all_tac HOL_basic_ss [@{thm unit_all_eq1}]);
    18.9      val cases = timeit_msg "record cases proof:" cases_prf;
   18.10  
   18.11      fun surjective_prf () =
    19.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Wed May 26 21:20:18 2010 +0200
    19.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Thu May 27 08:02:02 2010 +0200
    19.3 @@ -276,13 +276,13 @@
    19.4  OldGoals.by (REPEAT (dtac eq_reflection 1));
    19.5  (* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *)
    19.6  OldGoals.by (full_simp_tac ((global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs)
    19.7 -                              delsimps [not_iff,split_part])
    19.8 +                              delsimps [not_iff, @{thm split_part}])
    19.9                                addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @
   19.10                                          rename_simps @ ioa_simps @ asig_simps)) 1);
   19.11  OldGoals.by (full_simp_tac
   19.12 -  (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1);
   19.13 +  (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff, @{thm split_part}]) 1);
   19.14  OldGoals.by (REPEAT (if_full_simp_tac
   19.15 -  (global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1));
   19.16 +  (global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff, @{thm split_part}]) 1));
   19.17  OldGoals.by (call_mucke_tac 1);
   19.18  (* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *)
   19.19  OldGoals.by (atac 1);
    20.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Wed May 26 21:20:18 2010 +0200
    20.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Thu May 27 08:02:02 2010 +0200
    20.3 @@ -1101,7 +1101,7 @@
    20.4    THEN (REPEAT_DETERM (CHANGED (asm_simp_tac (simpset_of ctxt) i)));
    20.5  
    20.6  fun pair_tac ctxt s =
    20.7 -  res_inst_tac ctxt [(("p", 0), s)] PairE
    20.8 +  res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}
    20.9    THEN' hyp_subst_tac THEN' asm_full_simp_tac (simpset_of ctxt);
   20.10  
   20.11  (* induction on a sequence of pairs with pairsplitting and simplification *)