# HG changeset patch
# User oheimb
# Date 906372074 -7200
# Node ID 903c956beac3d8087a6ecf4167719c24eee668f9
# Parent  324e1560a5c9ad3230debc7f7969a09297419805
simplified proof

diff -r 324e1560a5c9 -r 903c956beac3 src/HOL/IMP/Hoare.ML
--- a/src/HOL/IMP/Hoare.ML	Mon Sep 21 10:46:58 1998 +0200
+++ b/src/HOL/IMP/Hoare.ML	Mon Sep 21 12:01:14 1998 +0200
@@ -9,7 +9,8 @@
 
 Goal "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}";
 by (etac hoare.conseq 1);
-by  (ALLGOALS Fast_tac);
+by  (atac 1);
+by (Fast_tac 1);
 qed "hoare_conseq1";
 
 Goal "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}";