| changeset 5515 | 903c956beac3 |
| parent 5301 | e24d15594edd |
| child 9241 | f961c1fdff50 |
--- 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'}";