# HG changeset patch
# User paulson
# Date 905523940 -7200
# Node ID 5a5dfb0f0d7db402f87020737a806dac118f339d
# Parent  33fcf0e60547aab19011d0dfa13103d4061fa0ae
fixed PROOF FAILED

diff -r 33fcf0e60547 -r 5a5dfb0f0d7d src/HOL/Auth/Kerberos_BAN.ML
--- a/src/HOL/Auth/Kerberos_BAN.ML	Fri Sep 11 16:25:24 1998 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.ML	Fri Sep 11 16:25:40 1998 +0200
@@ -255,7 +255,7 @@
 by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj,
                                Crypt_Spy_analz_bad, analz.Fst, analz.Snd]
                         addIs [less_SucI]) 1);
-val lemma = result() RS mp RS mp RSN(1,rev_notE);
+qed_spec_mp "lemma2";
 
 
 (** CONFIDENTIALITY for the SERVER:
@@ -268,8 +268,7 @@
 \        A ~: bad;  B ~: bad;  evs : kerberos_ban                \
 \     |] ==> Key K ~: analz (spies evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
-by (Clarify_tac 1);   (*prevents PROOF FAILED*)
-by (blast_tac (claset() addSEs [lemma]) 1);
+by (blast_tac (claset() addIs [lemma2]) 1);
 qed "Confidentiality_S";
 
 (**** THE COUNTERPART OF CONFIDENTIALITY 
diff -r 33fcf0e60547 -r 5a5dfb0f0d7d src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Fri Sep 11 16:25:24 1998 +0200
+++ b/src/HOL/Trancl.ML	Fri Sep 11 16:25:40 1998 +0200
@@ -133,9 +133,8 @@
 qed "rtrancl_subset";
 
 Goal "(R^* Un S^*)^* = (R Un S)^*";
-(*Blast_tac: PROOF FAILED*)
-by (Blast.depth_tac (claset() addSIs [rtrancl_subset]
-                       addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 4 1);
+by (blast_tac (claset() addSIs [rtrancl_subset]
+                        addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1);
 qed "rtrancl_Un_rtrancl";
 
 Goal "(R^=)^* = R^*";
diff -r 33fcf0e60547 -r 5a5dfb0f0d7d src/HOL/UNITY/Lift.ML
--- a/src/HOL/UNITY/Lift.ML	Fri Sep 11 16:25:24 1998 +0200
+++ b/src/HOL/UNITY/Lift.ML	Fri Sep 11 16:25:40 1998 +0200
@@ -425,9 +425,8 @@
 \     LeadsTo Lprg \
 \       (moving Int Req n Int (metric n -`` {N}) Int {s. floor s : req s})   \
 \       (moving Int Req n Int (metric n -`` lessThan N))";
-(*Blast_tac: PROOF FAILED*)
-by (best_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5]
-	               addIs [LeadsTo_Trans]) 1);
+by (blast_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5]
+	                addIs [LeadsTo_Trans]) 1);
 qed "lift_3_Req";
 
 
diff -r 33fcf0e60547 -r 5a5dfb0f0d7d src/HOL/UNITY/SubstAx.ML
--- a/src/HOL/UNITY/SubstAx.ML	Fri Sep 11 16:25:24 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML	Fri Sep 11 16:25:40 1998 +0200
@@ -100,7 +100,6 @@
 Goal "[| LeadsTo prg A A'; id: Acts prg;   \
 \        B  <= A;   A' <= B' |] \
 \     ==> LeadsTo prg B B'";
-(*PROOF FAILED unless the Trans rule is last*)
 by (blast_tac (claset() addIs [LeadsTo_weaken_R, LeadsTo_weaken_L,
 			       LeadsTo_Trans]) 1);
 qed "LeadsTo_weaken";
@@ -177,11 +176,7 @@
   This is the most useful form of the "disjunction" rule*)
 Goal "[| LeadsTo prg (A-B) C; LeadsTo prg (A Int B) C; id: Acts prg |] \
 \     ==> LeadsTo prg A C";
-by (stac (Un_Diff_Int RS sym) 1 THEN rtac LeadsTo_Un 1);
-by (REPEAT (assume_tac 1));
-(*One step, but PROOF FAILED...
-  by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
-*)
+by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
 qed "LeadsTo_Diff";
 
 
diff -r 33fcf0e60547 -r 5a5dfb0f0d7d src/HOL/UNITY/WFair.ML
--- a/src/HOL/UNITY/WFair.ML	Fri Sep 11 16:25:24 1998 +0200
+++ b/src/HOL/UNITY/WFair.ML	Fri Sep 11 16:25:40 1998 +0200
@@ -172,7 +172,6 @@
 
 Goal "[| leadsTo acts A A'; id: acts; B<=A; A'<=B' |] \
 \   ==> leadsTo acts B B'";
-(*PROOF FAILED unless leadsTo_Trans is last*)
 by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L,
 			       leadsTo_Trans]) 1);
 qed "leadsTo_weaken";
@@ -490,8 +489,7 @@
 by (subgoal_tac "leadsTo acts (A Int B) (A Int wlt acts B')" 1);
 by (blast_tac (claset() addIs [leadsTo_subset RS subsetD, 
 			       subset_imp_leadsTo]) 2);
-(*addIs looks safer, but loops with PROOF FAILED*)
-by (blast_tac (claset() addSIs [leadsTo_Trans]) 1);
+by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
 qed "stable_completion";
 
 
diff -r 33fcf0e60547 -r 5a5dfb0f0d7d src/HOL/ex/Puzzle.ML
--- a/src/HOL/ex/Puzzle.ML	Fri Sep 11 16:25:24 1998 +0200
+++ b/src/HOL/ex/Puzzle.ML	Fri Sep 11 16:25:40 1998 +0200
@@ -40,10 +40,7 @@
 by (res_inst_tac[("n","n")]nat_induct 1);
 by (Simp_tac 1);
 by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
-  (*Blast_tac: PROOF FAILED.  Perhaps remove DETERM for unsafe tactics,
-    or stop rotating prems for recursive rules: the le-assumptions
-    have got out of order.*)
-by (best_tac (claset() addIs (le_trans::prems)) 1);
+by (blast_tac (claset() addIs (le_trans::prems)) 1);
 qed_spec_mp "mono_lemma1";
 
 val [p1,p2] = goal Puzzle.thy
diff -r 33fcf0e60547 -r 5a5dfb0f0d7d src/ZF/Nat.ML
--- a/src/ZF/Nat.ML	Fri Sep 11 16:25:24 1998 +0200
+++ b/src/ZF/Nat.ML	Fri Sep 11 16:25:40 1998 +0200
@@ -175,9 +175,9 @@
 Goal "m: nat ==> P(m,succ(m)) --> (ALL x: nat. P(m,x) --> P(m,succ(x))) --> \
 \                 (ALL n:nat. m<n --> P(m,n))";
 by (etac nat_induct 1);
-by (ALLGOALS    (*blast_tac gives PROOF FAILED*)
+by (ALLGOALS   
     (EVERY' [rtac (impI RS impI), rtac (nat_induct RS ballI), assume_tac,
-             best_tac le_cs, best_tac le_cs])); 
+             blast_tac le_cs, blast_tac le_cs])); 
 qed "succ_lt_induct_lemma";
 
 val prems = goal Nat.thy
diff -r 33fcf0e60547 -r 5a5dfb0f0d7d src/ZF/Univ.ML
--- a/src/ZF/Univ.ML	Fri Sep 11 16:25:24 1998 +0200
+++ b/src/ZF/Univ.ML	Fri Sep 11 16:25:40 1998 +0200
@@ -404,9 +404,8 @@
 qed "Pow_in_Vfrom";
 
 Goal "[| a: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Pow(a) : Vfrom(A,i)";
-(*Blast_tac: PROOF FAILED*)
-by (fast_tac (claset() addEs [Limit_VfromE]
-		       addIs [Limit_has_succ, Pow_in_Vfrom, Limit_VfromI]) 1);
+by (blast_tac (claset() addEs [Limit_VfromE]
+		        addIs [Limit_has_succ, Pow_in_Vfrom, Limit_VfromI]) 1);
 qed "Pow_in_VLimit";