| changeset 4153 | e534c4c32d54 |
| parent 4089 | 96fba19bcbe2 |
| child 4241 | 3f3f87c6fe3b |
--- a/src/HOL/IMP/Hoare.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/IMP/Hoare.ML Wed Nov 05 13:23:46 1997 +0100 @@ -71,7 +71,7 @@ by (rtac iffI 1); by (rtac weak_coinduct 1); by (etac CollectI 1); - by (safe_tac (claset())); + by Safe_tac; by (rotate_tac ~1 1); by (Asm_full_simp_tac 1); by (rotate_tac ~1 1);