dropped axclass, going back to purely syntactic type classes

--- a/src/HOL/TLA/Action.thy	Tue Feb 23 10:11:15 2010 +0100
+++ b/src/HOL/TLA/Action.thy	Tue Feb 23 10:11:16 2010 +0100
@@ -16,8 +16,8 @@
   'a trfun = "(state * state) => 'a"
   action   = "bool trfun"
 
-instance
-  "*" :: (world, world) world ..
+arities
+  "*" :: (world, world) world
 
 consts
   (** abstract syntax **)

--- a/src/HOL/TLA/Init.thy	Tue Feb 23 10:11:15 2010 +0100
+++ b/src/HOL/TLA/Init.thy	Tue Feb 23 10:11:16 2010 +0100
@@ -12,7 +12,7 @@
 begin
 
 typedecl behavior
-instance behavior :: world ..
+arities behavior :: world
 
 types
   temporal = "behavior form"

--- a/src/HOL/TLA/Intensional.thy	Tue Feb 23 10:11:15 2010 +0100
+++ b/src/HOL/TLA/Intensional.thy	Tue Feb 23 10:11:16 2010 +0100
@@ -10,8 +10,8 @@
 imports Main
 begin
 
-axclass
-  world < type
+classes world
+classrel world < type
 
 (** abstract syntax **)
 
@@ -171,7 +171,7 @@
   "_liftMem"    :: "[lift, lift] => lift"                ("(_/ \<in> _)" [50, 51] 50)
   "_liftNotMem" :: "[lift, lift] => lift"                ("(_/ \<notin> _)" [50, 51] 50)
 
-axioms
+defs
   Valid_def:   "|- A    ==  ALL w. w |= A"
 
   unl_con:     "LIFT #c w  ==  c"

--- a/src/HOL/TLA/Stfun.thy	Tue Feb 23 10:11:15 2010 +0100
+++ b/src/HOL/TLA/Stfun.thy	Tue Feb 23 10:11:16 2010 +0100
@@ -11,7 +11,7 @@
 
 typedecl state
 
-instance state :: world ..
+arities state :: world
 
 types
   'a stfun = "state => 'a"