prefer antiquotations;
authorwenzelm
Mon Jan 09 18:29:42 2012 +0100 (2012-01-09)
changeset 461614ed94d92ae19
parent 46160 f363e5a2f8e8
child 46163 6c880b26dfc4
prefer antiquotations;
src/HOL/HOL.thy
src/HOL/HOLCF/Tools/cont_proc.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Prolog/prolog.ML
     1.1 --- a/src/HOL/HOL.thy	Mon Jan 09 14:47:18 2012 +0100
     1.2 +++ b/src/HOL/HOL.thy	Mon Jan 09 18:29:42 2012 +0100
     1.3 @@ -2008,37 +2008,6 @@
     1.4    fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
     1.5  end;
     1.6  
     1.7 -val case_split = @{thm case_split};
     1.8 -val cong = @{thm cong};
     1.9 -val de_Morgan_conj = @{thm de_Morgan_conj};
    1.10 -val de_Morgan_disj = @{thm de_Morgan_disj};
    1.11 -val disj_assoc = @{thm disj_assoc};
    1.12 -val disj_comms = @{thms disj_comms};
    1.13 -val disj_cong = @{thm disj_cong};
    1.14 -val eq_ac = @{thms eq_ac};
    1.15 -val eq_cong2 = @{thm eq_cong2}
    1.16 -val Eq_FalseI = @{thm Eq_FalseI};
    1.17 -val Eq_TrueI = @{thm Eq_TrueI};
    1.18 -val Ex1_def = @{thm Ex1_def};
    1.19 -val ex_disj_distrib = @{thm ex_disj_distrib};
    1.20 -val ex_simps = @{thms ex_simps};
    1.21 -val if_cancel = @{thm if_cancel};
    1.22 -val if_eq_cancel = @{thm if_eq_cancel};
    1.23 -val if_False = @{thm if_False};
    1.24 -val iff_conv_conj_imp = @{thm iff_conv_conj_imp};
    1.25 -val iff = @{thm iff};
    1.26 -val if_splits = @{thms if_splits};
    1.27 -val if_True = @{thm if_True};
    1.28 -val if_weak_cong = @{thm if_weak_cong};
    1.29 -val imp_all = @{thm imp_all};
    1.30 -val imp_cong = @{thm imp_cong};
    1.31 -val imp_conjL = @{thm imp_conjL};
    1.32 -val imp_conjR = @{thm imp_conjR};
    1.33 -val imp_conv_disj = @{thm imp_conv_disj};
    1.34 -val split_if = @{thm split_if};
    1.35 -val the1_equality = @{thm the1_equality};
    1.36 -val theI = @{thm theI};
    1.37 -val theI' = @{thm theI'};
    1.38  val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms nnf_simps});
    1.39  *}
    1.40  
     2.1 --- a/src/HOL/HOLCF/Tools/cont_proc.ML	Mon Jan 09 14:47:18 2012 +0100
     2.2 +++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Mon Jan 09 18:29:42 2012 +0100
     2.3 @@ -121,7 +121,7 @@
     2.4  local
     2.5    fun solve_cont thy _ t =
     2.6      let
     2.7 -      val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI
     2.8 +      val tr = instantiate' [] [SOME (cterm_of thy t)] @{thm Eq_TrueI}
     2.9      in Option.map fst (Seq.pull (cont_tac 1 tr)) end
    2.10  in
    2.11    fun cont_proc thy =
     3.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Mon Jan 09 14:47:18 2012 +0100
     3.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Mon Jan 09 18:29:42 2012 +0100
     3.3 @@ -982,7 +982,7 @@
     3.4                   else foldr1 (HOLogic.mk_binop @{const_abbrev union}) (map supp args2)))))
     3.5              (fn _ =>
     3.6                simp_tac (HOL_basic_ss addsimps (supp_def ::
     3.7 -                 Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
     3.8 +                 Un_assoc :: @{thm de_Morgan_conj} :: Collect_disj_eq :: finite_Un ::
     3.9                   Collect_False_empty :: finite_emptyI :: @{thms simp_thms} @
    3.10                   abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1)
    3.11          in
    3.12 @@ -1968,7 +1968,7 @@
    3.13                    end) context 1])) idxss) (ndescr ~~ rec_elims))
    3.14           end));
    3.15  
    3.16 -    val rec_total_thms = map (fn r => r RS theI') rec_unique_thms;
    3.17 +    val rec_total_thms = map (fn r => r RS @{thm theI'}) rec_unique_thms;
    3.18  
    3.19      (* define primrec combinators *)
    3.20  
    3.21 @@ -2011,7 +2011,7 @@
    3.22            (augment_sort thy12 fs_cp_sort concl')
    3.23            (fn {prems, ...} => EVERY
    3.24              [rewrite_goals_tac reccomb_defs,
    3.25 -             rtac the1_equality 1,
    3.26 +             rtac @{thm the1_equality} 1,
    3.27               solve rec_unique_thms prems 1,
    3.28               resolve_tac rec_intrs 1,
    3.29               REPEAT (solve (prems @ rec_total_thms) prems 1)])
     4.1 --- a/src/HOL/Prolog/prolog.ML	Mon Jan 09 14:47:18 2012 +0100
     4.2 +++ b/src/HOL/Prolog/prolog.ML	Mon Jan 09 18:29:42 2012 +0100
     4.3 @@ -63,9 +63,9 @@
     4.4      |> Simplifier.set_mksimps (mksimps mksimps_pairs))
     4.5    addsimps [
     4.6          @{thm all_conj_distrib}, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
     4.7 -        imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
     4.8 -        imp_conjR,        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
     4.9 -        imp_all];         (* "((!x. D) :- G) = (!x. D :- G)" *)
    4.10 +        @{thm imp_conjL} RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
    4.11 +        @{thm imp_conjR},        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
    4.12 +        @{thm imp_all}];         (* "((!x. D) :- G) = (!x. D :- G)" *)
    4.13  
    4.14  
    4.15  (*val hyp_resolve_tac = Subgoal.FOCUS_PREMS (fn {prems, ...} =>