--- a/src/HOL/Nat.thy Thu Jun 11 00:13:25 2015 +0100
+++ b/src/HOL/Nat.thy Thu Jun 11 18:24:44 2015 +0200
@@ -1881,12 +1881,12 @@
intro: order_trans[OF _ funpow_mono])
lemma mono_funpow:
- fixes Q :: "('i \<Rightarrow> 'a::{lattice, order_bot}) \<Rightarrow> ('i \<Rightarrow> 'a)"
+ fixes Q :: "'a::{lattice, order_bot} \<Rightarrow> 'a"
shows "mono Q \<Longrightarrow> mono (\<lambda>i. (Q ^^ i) \<bottom>)"
by (auto intro!: funpow_decreasing simp: mono_def)
lemma antimono_funpow:
- fixes Q :: "('i \<Rightarrow> 'a::{lattice, order_top}) \<Rightarrow> ('i \<Rightarrow> 'a)"
+ fixes Q :: "'a::{lattice, order_top} \<Rightarrow> 'a"
shows "mono Q \<Longrightarrow> antimono (\<lambda>i. (Q ^^ i) \<top>)"
by (auto intro!: funpow_increasing simp: antimono_def)