Deleted instance "set :: (type) power" and moved instance
authorberghofe
Wed May 07 10:56:41 2008 +0200 (2008-05-07)
changeset 267995bd38256ce5b
parent 26798 a9134a089106
child 26800 dcf1dfc915a7
Deleted instance "set :: (type) power" and moved instance
"fun :: (type, type) power" to the beginning of the theory
src/HOL/Relation_Power.thy
     1.1 --- a/src/HOL/Relation_Power.thy	Wed May 07 10:56:40 2008 +0200
     1.2 +++ b/src/HOL/Relation_Power.thy	Wed May 07 10:56:41 2008 +0200
     1.3 @@ -11,8 +11,8 @@
     1.4  begin
     1.5  
     1.6  instance
     1.7 -  set :: (type) power ..
     1.8 -      --{* only type @{typ "('a * 'a) set"} should be in class @{text power}!*}
     1.9 +  "fun" :: (type, type) power ..
    1.10 +      --{* only type @{typ "'a => 'a"} should be in class @{text power}!*}
    1.11  
    1.12  overloading
    1.13    relpow \<equiv> "power \<Colon> ('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a \<times> 'a) set"  (unchecked)
    1.14 @@ -26,10 +26,6 @@
    1.15  
    1.16  end
    1.17  
    1.18 -instance
    1.19 -  "fun" :: (type, type) power ..
    1.20 -      --{* only type @{typ "'a => 'a"} should be in class @{text power}!*}
    1.21 -
    1.22  overloading
    1.23    funpow \<equiv> "power \<Colon>  ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" (unchecked)
    1.24  begin