# HG changeset patch
# User paulson
# Date 863079592 -7200
# Node ID 2791aa6dc1bde3c90940dcc2d8d2532490f64eb4
# Parent  fb987fb6a489d5b3aa50ab148277861b932bf401
Changed from fast_tac to blast_tac

diff -r fb987fb6a489 -r 2791aa6dc1bd src/FOL/ex/If.ML
--- a/src/FOL/ex/If.ML	Wed May 07 18:39:04 1997 +0200
+++ b/src/FOL/ex/If.ML	Thu May 08 10:19:52 1997 +0200
@@ -3,7 +3,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
-For ex/if.thy.  First-Order Logic: the 'if' example
+First-Order Logic: the 'if' example
 *)
 
 open If;
@@ -11,13 +11,13 @@
 
 val prems = goalw If.thy [if_def]
     "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)";
-by (fast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
 qed "ifI";
 
 val major::prems = goalw If.thy [if_def]
    "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S";
 by (cut_facts_tac [major] 1);
-by (fast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
 qed "ifE";
 
 
@@ -32,30 +32,30 @@
 choplev 0;
 AddSIs [ifI];
 AddSEs [ifE];
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "if_commute";
 
 
 goal If.thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "nested_ifs";
 
 choplev 0;
 by (rewtac if_def);
-by (fast_tac FOL_cs 1);
+by (blast_tac FOL_cs 1);
 result();
 
 
 (*An invalid formula.  High-level rules permit a simpler diagnosis*)
 goal If.thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";
-by (Fast_tac 1) handle ERROR => writeln"Failed, as expected";
+by (Blast_tac 1) handle ERROR => writeln"Failed, as expected";
 (*Check that subgoals remain: proof failed.*)
 getgoal 1; 
 by (REPEAT (Step_tac 1));
 
 choplev 0;
 by (rewtac if_def);
-by (fast_tac FOL_cs 1) handle ERROR => writeln"Failed, as expected";
+by (blast_tac FOL_cs 1) handle ERROR => writeln"Failed, as expected";
 (*Check that subgoals remain: proof failed.*)
 getgoal 1; 
 by (REPEAT (step_tac FOL_cs 1));