| changeset 55380 | 4de48353034e |
| parent 41460 | ea56b98aee83 |
| child 58622 | aa99568f56de |
--- a/src/HOL/ex/Higher_Order_Logic.thy Mon Feb 10 14:33:47 2014 +0100 +++ b/src/HOL/ex/Higher_Order_Logic.thy Mon Feb 10 17:20:11 2014 +0100 @@ -18,13 +18,12 @@ subsection {* Pure Logic *} -classes type +class type default_sort type typedecl o -arities - o :: type - "fun" :: (type, type) type +instance o :: type .. +instance "fun" :: (type, type) type .. subsubsection {* Basic logical connectives *}