src/HOL/TLA/Intensional.thy
changeset 14565 c6dc17aab88a
parent 12338 de0f4a63baa5
child 17309 c43ed29bd197
     1.1 --- a/src/HOL/TLA/Intensional.thy	Wed Apr 14 13:28:46 2004 +0200
     1.2 +++ b/src/HOL/TLA/Intensional.thy	Wed Apr 14 14:13:05 2004 +0200
     1.3 @@ -162,7 +162,16 @@
     1.4    "_liftNotMem" :: [lift, lift] => lift                ("(_/ \\<notin> _)" [50, 51] 50)
     1.5  
     1.6  syntax (HTML output)
     1.7 +  "_liftNeq"    :: [lift, lift] => lift                (infixl "\\<noteq>" 50)
     1.8    "_liftNot"    :: lift => lift                        ("\\<not> _" [40] 40)
     1.9 +  "_liftAnd"    :: [lift, lift] => lift                (infixr "\\<and>" 35)
    1.10 +  "_liftOr"     :: [lift, lift] => lift                (infixr "\\<or>" 30)
    1.11 +  "_RAll"       :: [idts, lift] => lift                ("(3\\<forall>_./ _)" [0, 10] 10)
    1.12 +  "_REx"        :: [idts, lift] => lift                ("(3\\<exists>_./ _)" [0, 10] 10)
    1.13 +  "_REx1"       :: [idts, lift] => lift                ("(3\\<exists>!_./ _)" [0, 10] 10)
    1.14 +  "_liftLeq"    :: [lift, lift] => lift                ("(_/ \\<le> _)" [50, 51] 50)
    1.15 +  "_liftMem"    :: [lift, lift] => lift                ("(_/ \\<in> _)" [50, 51] 50)
    1.16 +  "_liftNotMem" :: [lift, lift] => lift                ("(_/ \\<notin> _)" [50, 51] 50)
    1.17  
    1.18  rules
    1.19    Valid_def   "|- A    ==  ALL w. w |= A"