src/HOLCF/IMP/Denotational.ML
changeset 3324 6b26b886ff69
parent 3221 90211fa9ee7e
child 3325 4e4ee8a101be
equal deleted inserted replaced
3323:194ae2e0c193 3324:6b26b886ff69
    35   by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
    35   by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
    36  by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
    36  by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
    37  by (fast_tac ((HOL_cs addIs evalc.intrs) addss !simpset) 1);
    37  by (fast_tac ((HOL_cs addIs evalc.intrs) addss !simpset) 1);
    38 by (Simp_tac 1);
    38 by (Simp_tac 1);
    39 br fix_ind 1;
    39 br fix_ind 1;
    40   by(fast_tac (HOL_cs addSIs (adm_lemmas@[adm_flatdom,flat_lift])) 1);
    40   by(fast_tac (HOL_cs addSIs (adm_lemmas@[adm_chfindom,flat_lift])) 1);
    41  by (Simp_tac 1);
    41  by (Simp_tac 1);
    42 by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
    42 by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
    43 by (safe_tac HOL_cs);
    43 by (safe_tac HOL_cs);
    44   by (fast_tac (HOL_cs addIs evalc.intrs) 1);
    44   by (fast_tac (HOL_cs addIs evalc.intrs) 1);
    45  by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
    45  by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);