Step_tac -> Safe_tac
authorpaulson
Mon, 29 Sep 1997 12:13:43 +0200
changeset 3737 3ea2f3b5e705
parent 3736 39ee3d31cfbc
child 3738 27f7473d029a
Step_tac -> Safe_tac
src/HOL/IMP/Hoare.ML
--- a/src/HOL/IMP/Hoare.ML	Mon Sep 29 11:56:04 1997 +0200
+++ b/src/HOL/IMP/Hoare.ML	Mon Sep 29 12:13:43 1997 +0200
@@ -96,7 +96,7 @@
 by (ALLGOALS Simp_tac);
 by (REPEAT_FIRST Fast_tac);
 by (deepen_tac (!claset addIs [hoare.conseq]) 0 1);
-by (Step_tac 1);
+by Safe_tac;
 by (rtac hoare.conseq 1);
   by (etac thin_rl 1);
   by (Fast_tac 1);