| changeset 4477 | b3e5857d8d99 |
| parent 4089 | 96fba19bcbe2 |
| child 5069 | 3ea049f7979d |
--- a/src/HOL/IMP/Denotation.ML Tue Dec 23 11:56:09 1997 +0100 +++ b/src/HOL/IMP/Denotation.ML Wed Dec 24 10:02:30 1997 +0100 @@ -29,7 +29,7 @@ (* start with rule induction *) by (etac evalc.induct 1); -by (Auto_tac()); +by Auto_tac; (* while *) by (rewtac Gamma_def); by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski)) 1);