Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/IMP/Denotational.ML
changeset 3325 4e4ee8a101be
parent 3324 6b26b886ff69
child 3457 a8ab7c64817c
equal deleted inserted replaced
3324:6b26b886ff69 3325:4e4ee8a101be 
    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_chfindom,flat_lift])) 1);
 
    40   by(fast_tac (HOL_cs addSIs (adm_lemmas@[adm_chfindom,ax_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);
isabelle