# 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));