Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
authorslotosch
Sun, 25 May 1997 16:57:19 +0200
changeset 3325 4e4ee8a101be
parent 3324 6b26b886ff69
child 3326 930c9bed5a09
*** empty log message ***
src/HOLCF/IMP/Denotational.ML file | annotate | diff | comparison | revisions 
--- 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);
isabelle