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)