| changeset 5143 | b94cd208f073 |
| parent 5068 | fb28eaa07e01 |
| child 5192 | 704dd3a6d47d |
--- a/src/HOLCF/IMP/Denotational.ML Tue Jul 14 13:33:12 1998 +0200 +++ b/src/HOLCF/IMP/Denotational.ML Wed Jul 15 10:15:13 1998 +0200 @@ -22,7 +22,7 @@ qed "dlift_is_Def"; Addsimps [dlift_is_Def]; -Goal "!!c. <c,s> -c-> t ==> D c`(Discr s) = (Def t)"; +Goal "<c,s> -c-> t ==> D c`(Discr s) = (Def t)"; by (etac evalc.induct 1); by (ALLGOALS Asm_simp_tac); by (ALLGOALS (stac fix_eq THEN' Asm_full_simp_tac));