src/HOL/HOL.thy
changeset 55383 a416780523e2
parent 55239 97921d23ebe3
child 55385 169e12bbf9a3
     1.1 --- a/src/HOL/HOL.thy	Mon Feb 10 21:00:56 2014 +0100
     1.2 +++ b/src/HOL/HOL.thy	Mon Feb 10 21:03:28 2014 +0100
     1.3 @@ -49,9 +49,11 @@
     1.4  default_sort type
     1.5  setup {* Object_Logic.add_base_sort @{sort type} *}
     1.6  
     1.7 -arities
     1.8 -  "fun" :: (type, type) type
     1.9 -  itself :: (type) type
    1.10 +axiomatization where fun_arity: "OFCLASS('a \<Rightarrow> 'b, type_class)"
    1.11 +instance "fun" :: (type, type) type by (rule fun_arity)
    1.12 +
    1.13 +axiomatization where itself_arity: "OFCLASS('a itself, type_class)"
    1.14 +instance itself :: (type) type by (rule itself_arity)
    1.15  
    1.16  typedecl bool
    1.17