Mercurial Mercurial > repos > isabelle / diff
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/Up1.ML
changeset 8161 bde1391fd0a5
parent 7294 5a50de9141b5
child 9169 85a47aa21f74 
--- a/src/HOLCF/Up1.ML	Fri Jan 28 14:49:00 2000 +0100
+++ b/src/HOLCF/Up1.ML	Fri Jan 28 15:08:15 2000 +0100
@@ -90,7 +90,8 @@
         (rtac refl 1)
         ]);
 
-val Up0_ss = (simpset_of Cfun3.thy) addsimps [Ifup1,Ifup2];
+val Up0_ss = (simpset_of Cfun3.thy) delsimps [range_composition] 
+	     addsimps [Ifup1,Ifup2];
 
 qed_goalw "less_up1a"  thy [less_up_def]
         "Abs_Up(Inl ())<< z"
isabelle