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/Ffun.thy
changeset 25923 5fe4b543512e
parent 25921 0ca392ab7f37
child 26025 ca6876116bb4 
--- a/src/HOLCF/Ffun.thy	Thu Jan 17 21:44:19 2008 +0100
+++ b/src/HOLCF/Ffun.thy	Thu Jan 17 21:56:33 2008 +0100
@@ -179,7 +179,7 @@
     \<Longrightarrow> monofun (\<Squnion>i. F i)"
 apply (rule monofunI)
 apply (simp add: thelub_fun)
-apply (rule lub_mono [rule_format])
+apply (rule lub_mono)
 apply (erule ch2ch_fun)
 apply (erule ch2ch_fun)
 apply (simp add: monofunE)
isabelle