generalized type signature to permit overloading on `set`
authorhaftmann
Sat Dec 24 15:53:09 2011 +0100 (2011-12-24)
changeset 459652af982715e5c
parent 45964 7b3a18670a9f
child 45966 03ce2b2a29a2
generalized type signature to permit overloading on `set`
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Nat.thy	Sat Dec 24 15:53:08 2011 +0100
     1.2 +++ b/src/HOL/Nat.thy	Sat Dec 24 15:53:09 2011 +0100
     1.3 @@ -1200,9 +1200,9 @@
     1.4    functions and relations, in order to share the same syntax.
     1.5  *}
     1.6  
     1.7 -consts compow :: "nat \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"
     1.8 +consts compow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
     1.9  
    1.10 -abbreviation compower :: "('a \<Rightarrow> 'b) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'b" (infixr "^^" 80) where
    1.11 +abbreviation compower :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^^" 80) where
    1.12    "f ^^ n \<equiv> compow n f"
    1.13  
    1.14  notation (latex output)