1.1 --- a/src/FOL/ex/If.ML	Wed May 07 18:39:04 1997 +0200
     1.2 +++ b/src/FOL/ex/If.ML	Thu May 08 10:19:52 1997 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1991  University of Cambridge
     1.6  
     1.7 -For ex/if.thy.  First-Order Logic: the 'if' example
     1.8 +First-Order Logic: the 'if' example
     1.9  *)
    1.10  
    1.11  open If;
    1.12 @@ -11,13 +11,13 @@
    1.13  
    1.14  val prems = goalw If.thy [if_def]
    1.15      "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)";
    1.16 -by (fast_tac (!claset addIs prems) 1);
    1.17 +by (blast_tac (!claset addIs prems) 1);
    1.18  qed "ifI";
    1.19  
    1.20  val major::prems = goalw If.thy [if_def]
    1.21     "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S";
    1.22  by (cut_facts_tac [major] 1);
    1.23 -by (fast_tac (!claset addIs prems) 1);
    1.24 +by (blast_tac (!claset addIs prems) 1);
    1.25  qed "ifE";
    1.26  
    1.27  
    1.28 @@ -32,30 +32,30 @@
    1.29  choplev 0;
    1.30  AddSIs [ifI];
    1.31  AddSEs [ifE];
    1.32 -by (Fast_tac 1);
    1.33 +by (Blast_tac 1);
    1.34  qed "if_commute";
    1.35  
    1.36  
    1.37  goal If.thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
    1.38 -by (Fast_tac 1);
    1.39 +by (Blast_tac 1);
    1.40  qed "nested_ifs";
    1.41  
    1.42  choplev 0;
    1.43  by (rewtac if_def);
    1.44 -by (fast_tac FOL_cs 1);
    1.45 +by (blast_tac FOL_cs 1);
    1.46  result();
    1.47  
    1.48  
    1.49  (*An invalid formula.  High-level rules permit a simpler diagnosis*)
    1.50  goal If.thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";
    1.51 -by (Fast_tac 1) handle ERROR => writeln"Failed, as expected";
    1.52 +by (Blast_tac 1) handle ERROR => writeln"Failed, as expected";
    1.53  (*Check that subgoals remain: proof failed.*)
    1.54  getgoal 1; 
    1.55  by (REPEAT (Step_tac 1));
    1.56  
    1.57  choplev 0;
    1.58  by (rewtac if_def);
    1.59 -by (fast_tac FOL_cs 1) handle ERROR => writeln"Failed, as expected";
    1.60 +by (blast_tac FOL_cs 1) handle ERROR => writeln"Failed, as expected";
    1.61  (*Check that subgoals remain: proof failed.*)
    1.62  getgoal 1; 
    1.63  by (REPEAT (step_tac FOL_cs 1));