--- a/src/HOL/Complex/ex/linrtac.ML Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/Complex/ex/linrtac.ML Thu Jul 05 20:01:26 2007 +0200
@@ -73,7 +73,7 @@
fun linr_tac ctxt q i =
- (ObjectLogic.atomize_tac i)
+ (ObjectLogic.atomize_prems_tac i)
THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] i))
THEN (fn st =>
let
--- a/src/HOL/Complex/ex/mirtac.ML Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/Complex/ex/mirtac.ML Thu Jul 05 20:01:26 2007 +0200
@@ -81,7 +81,7 @@
fun mir_tac ctxt q i =
- (ObjectLogic.atomize_tac i)
+ (ObjectLogic.atomize_prems_tac i)
THEN (simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i)
THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"},@{thm "abs_split"}] i))
THEN (fn st =>
@@ -161,4 +161,4 @@
"decision procedure for MIR arithmetic");
-end
\ No newline at end of file
+end
--- a/src/HOL/Nominal/nominal_package.ML Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Thu Jul 05 20:01:26 2007 +0200
@@ -1083,7 +1083,7 @@
(Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
(fn prems => EVERY
[rtac indrule_lemma' 1,
- (DatatypeAux.indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
+ (DatatypeAux.indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
EVERY (map (fn (prem, r) => (EVERY
[REPEAT (eresolve_tac Abs_inverse_thms' 1),
simp_tac (HOL_basic_ss addsimps [symmetric r]) 1,
--- a/src/HOL/Tools/datatype_abs_proofs.ML Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Thu Jul 05 20:01:26 2007 +0200
@@ -215,7 +215,7 @@
val induct' = cterm_instantiate ((map cert induct_Ps) ~~
(map cert insts)) induct;
val (tac, _) = Library.foldl mk_unique_tac
- (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_tac) 1
+ (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
THEN rewtac (mk_meta_eq choice_eq), rec_intrs),
descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
--- a/src/HOL/Tools/datatype_realizer.ML Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Thu Jul 05 20:01:26 2007 +0200
@@ -122,7 +122,7 @@
(fn prems =>
[rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
rtac (cterm_instantiate inst induction) 1,
- ALLGOALS ObjectLogic.atomize_tac,
+ ALLGOALS ObjectLogic.atomize_prems_tac,
rewrite_goals_tac (o_def :: map mk_meta_eq rec_rewrites),
REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
REPEAT (etac allE i) THEN atac i)) 1)]);
--- a/src/HOL/Tools/datatype_rep_proofs.ML Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Thu Jul 05 20:01:26 2007 +0200
@@ -403,7 +403,7 @@
val inj_thm = Goal.prove_global thy5 [] []
(HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
- [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
+ [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
REPEAT (EVERY
[rtac allI 1, rtac impI 1,
exh_tac (exh_thm_of dt_info) 1,
@@ -429,7 +429,7 @@
val elem_thm =
Goal.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
(fn _ =>
- EVERY [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
+ EVERY [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
rewrite_goals_tac rewrites,
REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
@@ -465,7 +465,7 @@
val iso_thms = if length descr = 1 then [] else
Library.drop (length newTs, split_conj_thm
(Goal.prove_global thy5 [] [] iso_t (fn _ => EVERY
- [(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
+ [(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
REPEAT (rtac TrueI 1),
rewrite_goals_tac (mk_meta_eq choice_eq ::
symmetric (mk_meta_eq expand_fun_eq) :: range_eqs),
@@ -606,7 +606,7 @@
(Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
(fn prems => EVERY
[rtac indrule_lemma' 1,
- (indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
+ (indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
EVERY (map (fn (prem, r) => (EVERY
[REPEAT (eresolve_tac Abs_inverse_thms 1),
simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
--- a/src/HOL/Tools/inductive_realizer.ML Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Thu Jul 05 20:01:26 2007 +0200
@@ -388,7 +388,7 @@
[rtac (#raw_induct ind_info) 1,
rewrite_goals_tac rews,
REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
- [K (rewrite_goals_tac rews), ObjectLogic.atomize_tac,
+ [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
val (thm', thy') = PureThy.store_thm ((space_implode "_"
(NameSpace.qualified qualifier "induct" :: vs @ Ps @
@@ -449,7 +449,7 @@
etac elimR 1,
ALLGOALS (asm_simp_tac HOL_basic_ss),
rewrite_goals_tac rews,
- REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_tac THEN'
+ REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN'
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
val (thm', thy') = PureThy.store_thm ((space_implode "_"
(name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy
--- a/src/HOL/Tools/meson.ML Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/Tools/meson.ML Thu Jul 05 20:01:26 2007 +0200
@@ -556,7 +556,7 @@
Function mkcl converts theorems to clauses.*)
fun MESON mkcl cltac i st =
SELECT_GOAL
- (EVERY [ObjectLogic.atomize_tac 1,
+ (EVERY [ObjectLogic.atomize_prems_tac 1,
rtac ccontr 1,
METAHYPS (fn negs =>
EVERY1 [skolemize_prems_tac negs,
--- a/src/HOL/Tools/res_atp_methods.ML Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/Tools/res_atp_methods.ML Thu Jul 05 20:01:26 2007 +0200
@@ -9,7 +9,7 @@
(* convert the negated 1st subgoal into CNF, write to file and call an ATP oracle *)
fun res_atp_tac dfg res_atp_oracle mode timeLimit ctxt user_thms n thm =
- (EVERY' [rtac ccontr,ObjectLogic.atomize_tac, skolemize_tac,
+ (EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, skolemize_tac,
METAHYPS(fn negs =>
HEADGOAL(Tactic.rtac
(res_atp_oracle (ProofContext.theory_of ctxt)
--- a/src/HOL/Tools/sat_funcs.ML Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Thu Jul 05 20:01:26 2007 +0200
@@ -428,7 +428,7 @@
val pre_cnf_tac =
rtac ccontr THEN'
- ObjectLogic.atomize_tac THEN'
+ ObjectLogic.atomize_prems_tac THEN'
CONVERSION Drule.beta_eta_conversion;
(* ------------------------------------------------------------------------- *)
--- a/src/HOL/ex/coopertac.ML Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/ex/coopertac.ML Thu Jul 05 20:01:26 2007 +0200
@@ -65,7 +65,7 @@
fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
-fun linz_tac ctxt q i = ObjectLogic.atomize_tac i THEN (fn st =>
+fun linz_tac ctxt q i = ObjectLogic.atomize_prems_tac i THEN (fn st =>
let
val g = List.nth (prems_of st, i - 1)
val thy = ProofContext.theory_of ctxt
@@ -140,4 +140,4 @@
linz_args linz_method,
"decision procedure for linear integer arithmetic");
-end
\ No newline at end of file
+end
--- a/src/Pure/Isar/method.ML Thu Jul 05 19:59:01 2007 +0200
+++ b/src/Pure/Isar/method.ML Thu Jul 05 20:01:26 2007 +0200
@@ -196,7 +196,7 @@
(* atomize rule statements *)
-fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o ObjectLogic.atomize_tac)
+fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o ObjectLogic.atomize_prems_tac)
| atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o ObjectLogic.full_atomize_tac)));
@@ -525,7 +525,7 @@
bang_sectioned_args' iprover_modifiers (Scan.lift (Scan.option Args.nat))
(fn n => fn prems => fn ctxt => METHOD (fn facts =>
HEADGOAL (insert_tac (prems @ facts) THEN'
- ObjectLogic.atomize_tac THEN' iprover_tac ctxt n)));
+ ObjectLogic.atomize_prems_tac THEN' iprover_tac ctxt n)));
end;