--- a/src/HOL/Nat.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Nat.thy Thu Jul 25 08:57:16 2013 +0200
@@ -444,7 +444,7 @@
end
-instantiation nat :: bot
+instantiation nat :: order_bot
begin
definition bot_nat :: nat where
@@ -1318,7 +1318,8 @@
subsection {* Kleene iteration *}
-lemma Kleene_iter_lpfp: assumes "mono f" and "f p \<le> p" shows "(f^^k) bot \<le> p"
+lemma Kleene_iter_lpfp:
+assumes "mono f" and "f p \<le> p" shows "(f^^k) (bot::'a::order_bot) \<le> p"
proof(induction k)
case 0 show ?case by simp
next