--- a/src/HOL/HOL.thy Fri Nov 23 21:09:32 2007 +0100
+++ b/src/HOL/HOL.thy Fri Nov 23 21:09:33 2007 +0100
@@ -38,16 +38,19 @@
classes type
defaultsort type
+setup {*
+ Typedecl.interpretation (fn a => fn thy => AxClass.axiomatize_arity
+ (a, replicate (Sign.arity_number thy a) @{sort type}, @{sort type}) thy)
+*}
+
+arities
+ "fun" :: (type, type) type
+ itself :: (type) type
+
global
typedecl bool
-arities
- bool :: type
- "fun" :: (type, type) type
-
- itself :: (type) type
-
judgment
Trueprop :: "bool => prop" ("(_)" 5)