| changeset 4241 | 3f3f87c6fe3b |
| parent 4153 | e534c4c32d54 |
| child 4686 | 74a12e86b20b |
--- a/src/HOL/IMP/Hoare.ML Thu Nov 20 10:54:04 1997 +0100 +++ b/src/HOL/IMP/Hoare.ML Thu Nov 20 10:55:27 1997 +0100 @@ -95,7 +95,7 @@ by (com.induct_tac "c" 1); by (ALLGOALS Simp_tac); by (REPEAT_FIRST Fast_tac); -by (deepen_tac (claset() addIs [hoare.conseq]) 0 1); +by (blast_tac (claset() addIs [hoare.conseq]) 1); by Safe_tac; by (rtac hoare.conseq 1); by (etac thin_rl 1);