--- a/src/HOL/HOL.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/HOL.thy Sat Dec 01 18:52:32 2001 +0100
@@ -13,16 +13,16 @@
subsubsection {* Core syntax *}
-global
+classes type < logic
+defaultsort type
-classes "term" < logic
-defaultsort "term"
+global
typedecl bool
arities
- bool :: "term"
- fun :: ("term", "term") "term"
+ bool :: type
+ fun :: (type, type) type
judgment
Trueprop :: "bool => prop" ("(_)" 5)
@@ -145,12 +145,12 @@
subsubsection {* Generic algebraic operations *}
-axclass zero < "term"
-axclass one < "term"
-axclass plus < "term"
-axclass minus < "term"
-axclass times < "term"
-axclass inverse < "term"
+axclass zero < type
+axclass one < type
+axclass plus < type
+axclass minus < type
+axclass times < type
+axclass inverse < type
global
@@ -528,7 +528,7 @@
subsection {* Order signatures and orders *}
axclass
- ord < "term"
+ ord < type
syntax
"op <" :: "['a::ord, 'a] => bool" ("op <")