| changeset 3324 | 6b26b886ff69 |
| parent 3221 | 90211fa9ee7e |
| child 3325 | 4e4ee8a101be |
--- a/src/HOLCF/IMP/Denotational.ML Sun May 25 11:07:52 1997 +0200 +++ b/src/HOLCF/IMP/Denotational.ML Sun May 25 16:17:09 1997 +0200 @@ -37,7 +37,7 @@ by (fast_tac ((HOL_cs addIs evalc.intrs) addss !simpset) 1); by (Simp_tac 1); br fix_ind 1; - by(fast_tac (HOL_cs addSIs (adm_lemmas@[adm_flatdom,flat_lift])) 1); + by(fast_tac (HOL_cs addSIs (adm_lemmas@[adm_chfindom,flat_lift])) 1); by (Simp_tac 1); by (simp_tac (!simpset setloop (split_tac[expand_if])) 1); by (safe_tac HOL_cs);