--- a/src/HOL/Relation_Power.thy Wed May 07 10:56:40 2008 +0200
+++ b/src/HOL/Relation_Power.thy Wed May 07 10:56:41 2008 +0200
@@ -11,8 +11,8 @@
begin
instance
- set :: (type) power ..
- --{* only type @{typ "('a * 'a) set"} should be in class @{text power}!*}
+ "fun" :: (type, type) power ..
+ --{* only type @{typ "'a => 'a"} should be in class @{text power}!*}
overloading
relpow \<equiv> "power \<Colon> ('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a \<times> 'a) set" (unchecked)
@@ -26,10 +26,6 @@
end
-instance
- "fun" :: (type, type) power ..
- --{* only type @{typ "'a => 'a"} should be in class @{text power}!*}
-
overloading
funpow \<equiv> "power \<Colon> ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" (unchecked)
begin