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.
ax_flat;
authorwenzelm
Sat, 03 Nov 2001 01:44:26 +0100
changeset 12031 1b883fa9458e
parent 12030 46d57d0290a2
child 12032 0f6417c9a187
ax_flat;
src/HOLCF/IMP/Denotational.ML file | annotate | diff | comparison | revisions 
--- a/src/HOLCF/IMP/Denotational.ML	Sat Nov 03 01:41:26 2001 +0100
+++ b/src/HOLCF/IMP/Denotational.ML	Sat Nov 03 01:44:26 2001 +0100
@@ -18,7 +18,7 @@
 
 Goalw [dlift_def]
  "(dlift f$l = Def y) = (? x. l = Def x & f$(Discr x) = Def y)";
-by (simp_tac (simpset() addsplits [Lift1.lift.split]) 1);
+by (simp_tac (simpset() addsplits [lift.split]) 1);
 qed "dlift_is_Def";
 Addsimps [dlift_is_Def];
 
@@ -37,7 +37,7 @@
  by (Force_tac 1);
 by (Simp_tac 1);
 by (rtac fix_ind 1);
-  by (fast_tac (claset() addSIs adm_lemmas@[adm_chfindom,ax_flat_lift]) 1);
+  by (fast_tac (claset() addSIs adm_lemmas @ [adm_chfindom, ax_flat]) 1);
  by (Simp_tac 1);
 by (Simp_tac 1);
 by Safe_tac;
isabelle