1.1 --- a/src/HOL/Complex/ex/linrtac.ML Thu Jul 05 19:59:01 2007 +0200
1.2 +++ b/src/HOL/Complex/ex/linrtac.ML Thu Jul 05 20:01:26 2007 +0200
1.3 @@ -73,7 +73,7 @@
1.4
1.5
1.6 fun linr_tac ctxt q i =
1.7 - (ObjectLogic.atomize_tac i)
1.8 + (ObjectLogic.atomize_prems_tac i)
1.9 THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] i))
1.10 THEN (fn st =>
1.11 let
2.1 --- a/src/HOL/Complex/ex/mirtac.ML Thu Jul 05 19:59:01 2007 +0200
2.2 +++ b/src/HOL/Complex/ex/mirtac.ML Thu Jul 05 20:01:26 2007 +0200
2.3 @@ -81,7 +81,7 @@
2.4
2.5
2.6 fun mir_tac ctxt q i =
2.7 - (ObjectLogic.atomize_tac i)
2.8 + (ObjectLogic.atomize_prems_tac i)
2.9 THEN (simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i)
2.10 THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"},@{thm "abs_split"}] i))
2.11 THEN (fn st =>
2.12 @@ -161,4 +161,4 @@
2.13 "decision procedure for MIR arithmetic");
2.14
2.15
2.16 -end
2.17 \ No newline at end of file
2.18 +end
3.1 --- a/src/HOL/Nominal/nominal_package.ML Thu Jul 05 19:59:01 2007 +0200
3.2 +++ b/src/HOL/Nominal/nominal_package.ML Thu Jul 05 20:01:26 2007 +0200
3.3 @@ -1083,7 +1083,7 @@
3.4 (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
3.5 (fn prems => EVERY
3.6 [rtac indrule_lemma' 1,
3.7 - (DatatypeAux.indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
3.8 + (DatatypeAux.indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
3.9 EVERY (map (fn (prem, r) => (EVERY
3.10 [REPEAT (eresolve_tac Abs_inverse_thms' 1),
3.11 simp_tac (HOL_basic_ss addsimps [symmetric r]) 1,
4.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML Thu Jul 05 19:59:01 2007 +0200
4.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Thu Jul 05 20:01:26 2007 +0200
4.3 @@ -215,7 +215,7 @@
4.4 val induct' = cterm_instantiate ((map cert induct_Ps) ~~
4.5 (map cert insts)) induct;
4.6 val (tac, _) = Library.foldl mk_unique_tac
4.7 - (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_tac) 1
4.8 + (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
4.9 THEN rewtac (mk_meta_eq choice_eq), rec_intrs),
4.10 descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
4.11
5.1 --- a/src/HOL/Tools/datatype_realizer.ML Thu Jul 05 19:59:01 2007 +0200
5.2 +++ b/src/HOL/Tools/datatype_realizer.ML Thu Jul 05 20:01:26 2007 +0200
5.3 @@ -122,7 +122,7 @@
5.4 (fn prems =>
5.5 [rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
5.6 rtac (cterm_instantiate inst induction) 1,
5.7 - ALLGOALS ObjectLogic.atomize_tac,
5.8 + ALLGOALS ObjectLogic.atomize_prems_tac,
5.9 rewrite_goals_tac (o_def :: map mk_meta_eq rec_rewrites),
5.10 REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
5.11 REPEAT (etac allE i) THEN atac i)) 1)]);
6.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML Thu Jul 05 19:59:01 2007 +0200
6.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Thu Jul 05 20:01:26 2007 +0200
6.3 @@ -403,7 +403,7 @@
6.4
6.5 val inj_thm = Goal.prove_global thy5 [] []
6.6 (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
6.7 - [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
6.8 + [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
6.9 REPEAT (EVERY
6.10 [rtac allI 1, rtac impI 1,
6.11 exh_tac (exh_thm_of dt_info) 1,
6.12 @@ -429,7 +429,7 @@
6.13 val elem_thm =
6.14 Goal.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
6.15 (fn _ =>
6.16 - EVERY [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
6.17 + EVERY [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
6.18 rewrite_goals_tac rewrites,
6.19 REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
6.20 ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
6.21 @@ -465,7 +465,7 @@
6.22 val iso_thms = if length descr = 1 then [] else
6.23 Library.drop (length newTs, split_conj_thm
6.24 (Goal.prove_global thy5 [] [] iso_t (fn _ => EVERY
6.25 - [(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
6.26 + [(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
6.27 REPEAT (rtac TrueI 1),
6.28 rewrite_goals_tac (mk_meta_eq choice_eq ::
6.29 symmetric (mk_meta_eq expand_fun_eq) :: range_eqs),
6.30 @@ -606,7 +606,7 @@
6.31 (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
6.32 (fn prems => EVERY
6.33 [rtac indrule_lemma' 1,
6.34 - (indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
6.35 + (indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
6.36 EVERY (map (fn (prem, r) => (EVERY
6.37 [REPEAT (eresolve_tac Abs_inverse_thms 1),
6.38 simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
7.1 --- a/src/HOL/Tools/inductive_realizer.ML Thu Jul 05 19:59:01 2007 +0200
7.2 +++ b/src/HOL/Tools/inductive_realizer.ML Thu Jul 05 20:01:26 2007 +0200
7.3 @@ -388,7 +388,7 @@
7.4 [rtac (#raw_induct ind_info) 1,
7.5 rewrite_goals_tac rews,
7.6 REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
7.7 - [K (rewrite_goals_tac rews), ObjectLogic.atomize_tac,
7.8 + [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
7.9 DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
7.10 val (thm', thy') = PureThy.store_thm ((space_implode "_"
7.11 (NameSpace.qualified qualifier "induct" :: vs @ Ps @
7.12 @@ -449,7 +449,7 @@
7.13 etac elimR 1,
7.14 ALLGOALS (asm_simp_tac HOL_basic_ss),
7.15 rewrite_goals_tac rews,
7.16 - REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_tac THEN'
7.17 + REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN'
7.18 DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
7.19 val (thm', thy') = PureThy.store_thm ((space_implode "_"
7.20 (name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy
8.1 --- a/src/HOL/Tools/meson.ML Thu Jul 05 19:59:01 2007 +0200
8.2 +++ b/src/HOL/Tools/meson.ML Thu Jul 05 20:01:26 2007 +0200
8.3 @@ -556,7 +556,7 @@
8.4 Function mkcl converts theorems to clauses.*)
8.5 fun MESON mkcl cltac i st =
8.6 SELECT_GOAL
8.7 - (EVERY [ObjectLogic.atomize_tac 1,
8.8 + (EVERY [ObjectLogic.atomize_prems_tac 1,
8.9 rtac ccontr 1,
8.10 METAHYPS (fn negs =>
8.11 EVERY1 [skolemize_prems_tac negs,
9.1 --- a/src/HOL/Tools/res_atp_methods.ML Thu Jul 05 19:59:01 2007 +0200
9.2 +++ b/src/HOL/Tools/res_atp_methods.ML Thu Jul 05 20:01:26 2007 +0200
9.3 @@ -9,7 +9,7 @@
9.4
9.5 (* convert the negated 1st subgoal into CNF, write to file and call an ATP oracle *)
9.6 fun res_atp_tac dfg res_atp_oracle mode timeLimit ctxt user_thms n thm =
9.7 - (EVERY' [rtac ccontr,ObjectLogic.atomize_tac, skolemize_tac,
9.8 + (EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, skolemize_tac,
9.9 METAHYPS(fn negs =>
9.10 HEADGOAL(Tactic.rtac
9.11 (res_atp_oracle (ProofContext.theory_of ctxt)
10.1 --- a/src/HOL/Tools/sat_funcs.ML Thu Jul 05 19:59:01 2007 +0200
10.2 +++ b/src/HOL/Tools/sat_funcs.ML Thu Jul 05 20:01:26 2007 +0200
10.3 @@ -428,7 +428,7 @@
10.4
10.5 val pre_cnf_tac =
10.6 rtac ccontr THEN'
10.7 - ObjectLogic.atomize_tac THEN'
10.8 + ObjectLogic.atomize_prems_tac THEN'
10.9 CONVERSION Drule.beta_eta_conversion;
10.10
10.11 (* ------------------------------------------------------------------------- *)
11.1 --- a/src/HOL/ex/coopertac.ML Thu Jul 05 19:59:01 2007 +0200
11.2 +++ b/src/HOL/ex/coopertac.ML Thu Jul 05 20:01:26 2007 +0200
11.3 @@ -65,7 +65,7 @@
11.4 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
11.5
11.6
11.7 -fun linz_tac ctxt q i = ObjectLogic.atomize_tac i THEN (fn st =>
11.8 +fun linz_tac ctxt q i = ObjectLogic.atomize_prems_tac i THEN (fn st =>
11.9 let
11.10 val g = List.nth (prems_of st, i - 1)
11.11 val thy = ProofContext.theory_of ctxt
11.12 @@ -140,4 +140,4 @@
11.13 linz_args linz_method,
11.14 "decision procedure for linear integer arithmetic");
11.15
11.16 -end
11.17 \ No newline at end of file
11.18 +end
12.1 --- a/src/Pure/Isar/method.ML Thu Jul 05 19:59:01 2007 +0200
12.2 +++ b/src/Pure/Isar/method.ML Thu Jul 05 20:01:26 2007 +0200
12.3 @@ -196,7 +196,7 @@
12.4
12.5 (* atomize rule statements *)
12.6
12.7 -fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o ObjectLogic.atomize_tac)
12.8 +fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o ObjectLogic.atomize_prems_tac)
12.9 | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o ObjectLogic.full_atomize_tac)));
12.10
12.11
12.12 @@ -525,7 +525,7 @@
12.13 bang_sectioned_args' iprover_modifiers (Scan.lift (Scan.option Args.nat))
12.14 (fn n => fn prems => fn ctxt => METHOD (fn facts =>
12.15 HEADGOAL (insert_tac (prems @ facts) THEN'
12.16 - ObjectLogic.atomize_tac THEN' iprover_tac ctxt n)));
12.17 + ObjectLogic.atomize_prems_tac THEN' iprover_tac ctxt n)));
12.18
12.19 end;
12.20