--- a/src/HOL/Library/Order_Continuity.thy Sat Oct 01 12:03:27 2016 +0200
+++ b/src/HOL/Library/Order_Continuity.thy Sat Oct 01 17:16:35 2016 +0200
@@ -123,7 +123,7 @@
case (Suc i)
have "(F ^^ Suc i) bot = F ((F ^^ i) bot)" by simp
also have "\<dots> \<le> F (lfp F)" by (rule monoD[OF mono Suc])
- also have "\<dots> = lfp F" by (simp add: lfp_unfold[OF mono, symmetric])
+ also have "\<dots> = lfp F" by (simp add: lfp_fixpoint[OF mono])
finally show ?case .
qed simp
qed
@@ -287,7 +287,7 @@
fix i show "gfp F \<le> (F ^^ i) top"
proof (induct i)
case (Suc i)
- have "gfp F = F (gfp F)" by (simp add: gfp_unfold[OF mono, symmetric])
+ have "gfp F = F (gfp F)" by (simp add: gfp_fixpoint[OF mono])
also have "\<dots> \<le> F ((F ^^ i) top)" by (rule monoD[OF mono Suc])
also have "\<dots> = (F ^^ Suc i) top" by simp
finally show ?case .