changeset 17831 | 4a8c3f8b0a92 |
parent 16737 | f0fd06dc93e3 |
child 18088 | e5b23b85e932 |
--- a/src/HOLCF/Cont.thy Tue Oct 11 17:30:00 2005 +0200 +++ b/src/HOLCF/Cont.thy Tue Oct 11 23:19:50 2005 +0200 @@ -215,7 +215,7 @@ lemma mono2mono_MF1L_rev: "\<forall>y. monofun (\<lambda>x. f x y) \<Longrightarrow> monofun f" apply (rule monofunI) -apply (rule less_fun [THEN iffD2]) +apply (rule less_fun_ext) apply (blast dest: monofunE) done