more explicit axiomatization;
authorwenzelm
Mon Feb 10 21:03:28 2014 +0100 (2014-02-10)
changeset 55383a416780523e2
parent 55382 9218fa411c15
child 55384 1107de77c633
more explicit axiomatization;
src/HOL/HOL.thy
     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