src/HOL/Nat.thy
changeset 60427 b4b672f09270
parent 60353 838025c6e278
child 60562 24af00b010cf
     1.1 --- a/src/HOL/Nat.thy	Thu Jun 11 00:13:25 2015 +0100
     1.2 +++ b/src/HOL/Nat.thy	Thu Jun 11 18:24:44 2015 +0200
     1.3 @@ -1881,12 +1881,12 @@
     1.4             intro: order_trans[OF _ funpow_mono])
     1.5  
     1.6  lemma mono_funpow:
     1.7 -  fixes Q :: "('i \<Rightarrow> 'a::{lattice, order_bot}) \<Rightarrow> ('i \<Rightarrow> 'a)"
     1.8 +  fixes Q :: "'a::{lattice, order_bot} \<Rightarrow> 'a"
     1.9    shows "mono Q \<Longrightarrow> mono (\<lambda>i. (Q ^^ i) \<bottom>)"
    1.10    by (auto intro!: funpow_decreasing simp: mono_def)
    1.11  
    1.12  lemma antimono_funpow:
    1.13 -  fixes Q :: "('i \<Rightarrow> 'a::{lattice, order_top}) \<Rightarrow> ('i \<Rightarrow> 'a)"
    1.14 +  fixes Q :: "'a::{lattice, order_top} \<Rightarrow> 'a"
    1.15    shows "mono Q \<Longrightarrow> antimono (\<lambda>i. (Q ^^ i) \<top>)"
    1.16    by (auto intro!: funpow_increasing simp: antimono_def)
    1.17