# HG changeset patch
# User haftmann
# Date 1266916276 -3600
# Node ID e1b61c5fd494a3bffbca9a05b6723a084b04f95d
# Parent  d57da4abb47d34f3d1573cea906ffe3421c73e4d
dropped axclass, going back to purely syntactic type classes

diff -r d57da4abb47d -r e1b61c5fd494 src/HOL/TLA/Action.thy
--- 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 **)
diff -r d57da4abb47d -r e1b61c5fd494 src/HOL/TLA/Init.thy
--- 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"
diff -r d57da4abb47d -r e1b61c5fd494 src/HOL/TLA/Intensional.thy
--- 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"
diff -r d57da4abb47d -r e1b61c5fd494 src/HOL/TLA/Stfun.thy
--- 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"