src/HOL/TLA/Intensional.thy
changeset 12114 a8e860c86252
parent 9517 f58863b1406a
child 12338 de0f4a63baa5
     1.1 --- a/src/HOL/TLA/Intensional.thy	Fri Nov 09 00:06:15 2001 +0100
     1.2 +++ b/src/HOL/TLA/Intensional.thy	Fri Nov 09 00:09:47 2001 +0100
     1.3 @@ -146,14 +146,14 @@
     1.4    "w |= EX x. A"   <= "_REx x A w"
     1.5    "w |= EX! x. A"  <= "_REx1 x A w"
     1.6  
     1.7 -syntax (symbols)
     1.8 +syntax (xsymbols)
     1.9    "_Valid"      :: lift => bool                        ("(\\<turnstile> _)" 5)
    1.10    "_holdsAt"    :: ['a, lift] => bool                  ("(_ \\<Turnstile> _)" [100,10] 10)
    1.11    "_liftNeq"    :: [lift, lift] => lift                (infixl "\\<noteq>" 50)
    1.12    "_liftNot"    :: lift => lift                        ("\\<not> _" [40] 40)
    1.13    "_liftAnd"    :: [lift, lift] => lift                (infixr "\\<and>" 35)
    1.14    "_liftOr"     :: [lift, lift] => lift                (infixr "\\<or>" 30)
    1.15 -  "_liftImp"    :: [lift, lift] => lift                (infixr "\\<midarrow>\\<rightarrow>" 25)
    1.16 +  "_liftImp"    :: [lift, lift] => lift                (infixr "\\<longrightarrow>" 25)
    1.17    "_RAll"       :: [idts, lift] => lift                ("(3\\<forall>_./ _)" [0, 10] 10)
    1.18    "_REx"        :: [idts, lift] => lift                ("(3\\<exists>_./ _)" [0, 10] 10)
    1.19    "_REx1"       :: [idts, lift] => lift                ("(3\\<exists>!_./ _)" [0, 10] 10)