src/HOL/Relation_Power.thy
changeset 26799 5bd38256ce5b
parent 26072 f65a7fa2da6c
child 28517 dd46786d4f95
     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