src/LCF/ex/Ex4.thy
changeset 58977 9576b510f6a2
parent 58974 cbc2ac19d783
child 60770 240563fbf41d
--- a/src/LCF/ex/Ex4.thy	Tue Nov 11 13:50:56 2014 +0100
+++ b/src/LCF/ex/Ex4.thy	Tue Nov 11 15:55:31 2014 +0100
@@ -6,7 +6,7 @@
 begin
 
 lemma example:
-  assumes asms: "f(p) << p"  "!!q. f(q) << q ==> p << q"
+  assumes asms: "f(p) << p"  "\<And>q. f(q) << q \<Longrightarrow> p << q"
   shows "FIX(f)=p"
   apply (unfold eq_def)
   apply (rule conjI)