--- a/src/HOL/Algebra/abstract/Ring.thy Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/Algebra/abstract/Ring.thy Fri Oct 21 18:14:34 2005 +0200
@@ -164,7 +164,7 @@
"t * u::'a::ring",
"- t::'a::ring"];
fun proc sg ss t =
- let val rew = Tactic.prove sg [] []
+ let val rew = Goal.prove sg [] []
(HOLogic.mk_Trueprop
(HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
(fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1)
--- a/src/HOL/Fun.thy Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/Fun.thy Fri Oct 21 18:14:34 2005 +0200
@@ -497,7 +497,7 @@
(fn sg => fn ss => fn t =>
case find_double t of (T, NONE) => NONE
| (T, SOME rhs) =>
- SOME (Tactic.prove sg [] [] (Term.equals T $ t $ rhs) (K (fun_upd_prover ss))))
+ SOME (Goal.prove sg [] [] (Term.equals T $ t $ rhs) (K (fun_upd_prover ss))))
end;
Addsimprocs[fun_upd2_simproc];
--- a/src/HOL/Hoare/hoare.ML Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/Hoare/hoare.ML Fri Oct 21 18:14:34 2005 +0200
@@ -82,7 +82,7 @@
Free ("P",varsT --> boolT) $ Bound 0));
val impl = implies $ (Mset_incl big_Collect) $
(Mset_incl small_Collect);
- in Tactic.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
+ in Goal.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
end;
--- a/src/HOL/Hoare/hoareAbort.ML Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/Hoare/hoareAbort.ML Fri Oct 21 18:14:34 2005 +0200
@@ -83,7 +83,7 @@
Free ("P",varsT --> boolT) $ Bound 0));
val impl = implies $ (Mset_incl big_Collect) $
(Mset_incl small_Collect);
- in Tactic.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
+ in Goal.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
end;
--- a/src/HOL/Hyperreal/transfer.ML Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/Hyperreal/transfer.ML Fri Oct 21 18:14:34 2005 +0200
@@ -72,7 +72,7 @@
, REPEAT_ALL_NEW (resolve_tac intros) 1
, match_tac [reflexive_thm] 1 ]
in
- prove_goalw_cterm (ths @ refolds @ unfolds) ct (fn _ => tacs)
+ OldGoals.prove_goalw_cterm (ths @ refolds @ unfolds) ct (fn _ => tacs)
end
fun transfer_tac ths =
--- a/src/HOL/IMPP/Hoare.ML Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/IMPP/Hoare.ML Fri Oct 21 18:14:34 2005 +0200
@@ -268,7 +268,7 @@
by (resolve_tac (premises()(*hoare_derivs.asm*)) 1);
by (Fast_tac 1);
by (resolve_tac (tl(premises())(*MGT_BodyN*)) 1);
-byev[dtac spec 1, etac impE 1, etac impE 2, dtac spec 3,etac mp 3];
+by (EVERY [dtac spec 1, etac impE 1, etac impE 2, dtac spec 3,etac mp 3]);
by (eresolve_tac (tl(tl(tl(premises())))) 3);
by (Fast_tac 1);
by (dtac finite_subset 1);
--- a/src/HOL/Integ/int_arith1.ML Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/Integ/int_arith1.ML Fri Oct 21 18:14:34 2005 +0200
@@ -96,7 +96,7 @@
if t aconv u then NONE
else
let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
- in SOME (Tactic.prove sg xs [] eq (K (EVERY tacs))) end
+ in SOME (Goal.prove sg xs [] eq (K (EVERY tacs))) end
fun prove_conv_nohyps tacs sg = prove_conv tacs sg [];
fun prove_conv_nohyps_novars tacs sg = prove_conv tacs sg [] [];
--- a/src/HOL/List.thy Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/List.thy Fri Oct 21 18:14:34 2005 +0200
@@ -453,7 +453,7 @@
val app = Const("List.op @",appT)
val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
- val thm = Tactic.prove sg [] [] eq
+ val thm = Goal.prove sg [] [] eq
(K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
--- a/src/HOL/Product_Type.thy Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/Product_Type.thy Fri Oct 21 18:14:34 2005 +0200
@@ -413,7 +413,7 @@
fun split_pat tp i (Abs (_,_,t)) = if tp 0 i t then SOME (i,t) else NONE
| split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t
| split_pat tp i _ = NONE;
- fun metaeq thy ss lhs rhs = mk_meta_eq (Tactic.prove thy [] []
+ fun metaeq thy ss lhs rhs = mk_meta_eq (Goal.prove thy [] []
(HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs)))
(K (simp_tac (Simplifier.inherit_context ss HOL_basic_ss addsimps [cond_split_eta]) 1)));
--- a/src/HOL/Tools/datatype_package.ML Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/Tools/datatype_package.ML Fri Oct 21 18:14:34 2005 +0200
@@ -347,10 +347,10 @@
in (case (#distinct (datatype_info_err sg tname1)) of
QuickAndDirty => SOME (Thm.invoke_oracle
Datatype_thy distinctN (sg, ConstrDistinct eq_t))
- | FewConstrs thms => SOME (Tactic.prove sg [] [] eq_t (K
+ | FewConstrs thms => SOME (Goal.prove sg [] [] eq_t (K
(EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
atac 2, resolve_tac thms 1, etac FalseE 1])))
- | ManyConstrs (thm, simpset) => SOME (Tactic.prove sg [] [] eq_t (K
+ | ManyConstrs (thm, simpset) => SOME (Goal.prove sg [] [] eq_t (K
(EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
full_simp_tac (Simplifier.inherit_context ss simpset) 1,
REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
--- a/src/HOL/Tools/typedef_package.ML Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/Tools/typedef_package.ML Fri Oct 21 18:14:34 2005 +0200
@@ -226,8 +226,8 @@
val (cset, goal, _, typedef_result) =
prepare_typedef prep_term def name typ set opt_morphs thy;
val _ = message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ...");
- val non_empty = Tactic.prove thy [] [] goal (K tac) handle ERROR =>
- error ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset));
+ val non_empty = Goal.prove thy [] [] goal (K tac) handle ERROR_MESSAGE msg =>
+ error (msg ^ "\nFailed to prove non-emptiness of " ^ quote (string_of_cterm cset));
val ((thy', _), result) = (thy, non_empty) |> typedef_result;
in (thy', result) end;
--- a/src/HOLCF/adm_tac.ML Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOLCF/adm_tac.ML Fri Oct 21 18:14:34 2005 +0200
@@ -102,7 +102,7 @@
| mk_all ((a,T)::Ts) t = (all T) $ (Abs (a, T, mk_all Ts t));
val t = HOLogic.mk_Trueprop((Const (cont_name, contT)) $ (Abs(s, T, t)));
val t' = mk_all params (Logic.list_implies (prems, t));
- val thm = Tactic.prove sign [] [] t' (K (tac 1));
+ val thm = Goal.prove sign [] [] t' (K (tac 1));
in (ts, thm)::l end
handle ERROR_MESSAGE _ => l;
--- a/src/Provers/Arith/abel_cancel.ML Fri Oct 21 18:14:32 2005 +0200
+++ b/src/Provers/Arith/abel_cancel.ML Fri Oct 21 18:14:34 2005 +0200
@@ -90,7 +90,7 @@
fun sum_proc sg ss t =
let val t' = cancel sg t
- val thm = Tactic.prove sg [] [] (Logic.mk_equals (t, t'))
+ val thm = Goal.prove sg [] [] (Logic.mk_equals (t, t'))
(fn _ => simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
in SOME thm end
handle Cancel => NONE;
@@ -110,7 +110,7 @@
fun rel_proc sg ss t =
let val t' = cancel sg t
- val thm = Tactic.prove sg [] [] (Logic.mk_equals (t, t'))
+ val thm = Goal.prove sg [] [] (Logic.mk_equals (t, t'))
(fn _ => rtac eq_reflection 1 THEN
resolve_tac eqI_rules 1 THEN
simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
--- a/src/Provers/Arith/assoc_fold.ML Fri Oct 21 18:14:32 2005 +0200
+++ b/src/Provers/Arith/assoc_fold.ML Fri Oct 21 18:14:34 2005 +0200
@@ -54,7 +54,7 @@
else ()
val rhs = plus $ mk_sum plus lits $ mk_sum plus others
val _ = if !trace then tracing ("RHS = " ^ show rhs) else ()
- val th = Tactic.prove thy [] [] (Logic.mk_equals (lhs, rhs))
+ val th = Goal.prove thy [] [] (Logic.mk_equals (lhs, rhs))
(fn _ => rtac Data.eq_reflection 1 THEN
simp_tac (Simplifier.inherit_context ss assoc_ss) 1)
in SOME th end
--- a/src/Provers/quantifier1.ML Fri Oct 21 18:14:32 2005 +0200
+++ b/src/Provers/quantifier1.ML Fri Oct 21 18:14:34 2005 +0200
@@ -104,7 +104,7 @@
in exqu end;
fun prove_conv tac thy tu =
- Tactic.prove thy [] [] (Logic.mk_equals tu) (K (rtac iff_reflection 1 THEN tac));
+ Goal.prove thy [] [] (Logic.mk_equals tu) (K (rtac iff_reflection 1 THEN tac));
fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i)
--- a/src/Pure/Isar/skip_proof.ML Fri Oct 21 18:14:32 2005 +0200
+++ b/src/Pure/Isar/skip_proof.ML Fri Oct 21 18:14:34 2005 +0200
@@ -35,7 +35,7 @@
ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
fun prove thy xs asms prop tac =
- Tactic.prove thy xs asms prop
+ Goal.prove thy xs asms prop
(if ! quick_and_dirty then (K (cheat_tac thy)) else tac);
end;
--- a/src/Pure/axclass.ML Fri Oct 21 18:14:32 2005 +0200
+++ b/src/Pure/axclass.ML Fri Oct 21 18:14:34 2005 +0200
@@ -272,8 +272,8 @@
val (c1, c2) = prep_classrel thy raw_cc;
val txt = quote (Sign.string_of_classrel thy [c1, c2]);
val _ = message ("Proving class inclusion " ^ txt ^ " ...");
- val th = Tactic.prove thy [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR =>
- error ("The error(s) above occurred while trying to prove " ^ txt);
+ val th = Goal.prove thy [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR_MESSAGE msg =>
+ error (msg ^ "\nThe error(s) above occurred while trying to prove " ^ txt);
in add_classrel_thms [th] thy end;
fun ext_inst_arity prep_arity raw_arity tac thy =
@@ -282,9 +282,9 @@
val txt = quote (Sign.string_of_arity thy arity);
val _ = message ("Proving type arity " ^ txt ^ " ...");
val props = (mk_arities arity);
- val ths = Tactic.prove_multi thy [] [] props
- (fn _ => Tactic.smart_conjunction_tac (length props) THEN tac)
- handle ERROR => error ("The error(s) above occurred while trying to prove " ^ txt);
+ val ths = Goal.prove_multi thy [] [] props
+ (fn _ => Tactic.smart_conjunction_tac (length props) THEN tac) handle ERROR_MESSAGE msg =>
+ error (msg ^ "\nThe error(s) above occurred while trying to prove " ^ txt);
in add_arity_thms ths thy end;
in
--- a/src/ZF/Datatype.ML Fri Oct 21 18:14:32 2005 +0200
+++ b/src/ZF/Datatype.ML Fri Oct 21 18:14:34 2005 +0200
@@ -87,7 +87,7 @@
writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new))
else ();
val goal = Logic.mk_equals (old, new)
- val thm = Tactic.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN
+ val thm = Goal.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN
simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1)
handle ERROR_MESSAGE msg =>
(warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal);
--- a/src/ZF/arith_data.ML Fri Oct 21 18:14:32 2005 +0200
+++ b/src/ZF/arith_data.ML Fri Oct 21 18:14:34 2005 +0200
@@ -74,7 +74,7 @@
let val hyps' = List.filter (not o is_eq_thm) hyps
val goal = Logic.list_implies (map (#prop o Thm.rep_thm) hyps',
FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
- in SOME (hyps' MRS Tactic.prove sg xs [] goal (K (EVERY tacs)))
+ in SOME (hyps' MRS Goal.prove sg xs [] goal (K (EVERY tacs)))
handle ERROR_MESSAGE msg =>
(warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); NONE)
end;