# HG changeset patch # User slotosch # Date 864572239 -7200 # Node ID 4e4ee8a101be9503cc163711f062f9901d7599a8 # Parent 6b26b886ff693bd37ec4a375c73e9170ae5447cc *** empty log message *** diff -r 6b26b886ff69 -r 4e4ee8a101be src/HOLCF/IMP/Denotational.ML --- a/src/HOLCF/IMP/Denotational.ML Sun May 25 16:17:09 1997 +0200 +++ b/src/HOLCF/IMP/Denotational.ML Sun May 25 16:57:19 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_chfindom,flat_lift])) 1); + by(fast_tac (HOL_cs addSIs (adm_lemmas@[adm_chfindom,ax_flat_lift])) 1); by (Simp_tac 1); by (simp_tac (!simpset setloop (split_tac[expand_if])) 1); by (safe_tac HOL_cs);