src/HOL/TLA/Intensional.thy
changeset 35318 e1b61c5fd494
parent 35108 e384e27c229f
child 35354 2e8dc3c64430
     1.1 --- a/src/HOL/TLA/Intensional.thy	Tue Feb 23 10:11:15 2010 +0100
     1.2 +++ b/src/HOL/TLA/Intensional.thy	Tue Feb 23 10:11:16 2010 +0100
     1.3 @@ -10,8 +10,8 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -axclass
     1.8 -  world < type
     1.9 +classes world
    1.10 +classrel world < type
    1.11  
    1.12  (** abstract syntax **)
    1.13  
    1.14 @@ -171,7 +171,7 @@
    1.15    "_liftMem"    :: "[lift, lift] => lift"                ("(_/ \<in> _)" [50, 51] 50)
    1.16    "_liftNotMem" :: "[lift, lift] => lift"                ("(_/ \<notin> _)" [50, 51] 50)
    1.17  
    1.18 -axioms
    1.19 +defs
    1.20    Valid_def:   "|- A    ==  ALL w. w |= A"
    1.21  
    1.22    unl_con:     "LIFT #c w  ==  c"