| changeset 3457 | a8ab7c64817c |
| parent 2036 | 62ff902eeffc |
| child 4089 | 96fba19bcbe2 |
--- a/src/HOL/IMP/Denotation.ML Mon Jun 23 10:35:49 1997 +0200 +++ b/src/HOL/IMP/Denotation.ML Mon Jun 23 10:42:03 1997 +0200 @@ -29,7 +29,7 @@ (* start with rule induction *) by (etac evalc.induct 1); -auto(); +by (Auto_tac()); (* while *) by (rewtac Gamma_def); by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski)) 1);