| changeset 10186 | 499637e8f2c6 |
| parent 9241 | f961c1fdff50 |
| child 10202 | 9e8b4bebc940 |
--- a/src/HOL/IMP/Hoare.ML Wed Oct 11 00:03:22 2000 +0200 +++ b/src/HOL/IMP/Hoare.ML Wed Oct 11 09:09:06 2000 +0200 @@ -87,7 +87,7 @@ by (assume_tac 2); by (etac induct2 1); by (fast_tac (claset() addSIs [monoI]) 1); -by (stac gfp_Tarski 1); +by (stac gfp_unfold 1); by (fast_tac (claset() addSIs [monoI]) 1); by (Fast_tac 1); qed "wp_While";