src/HOL/TLA/TLA.thy
changeset 12114 a8e860c86252
parent 9517 f58863b1406a
child 14565 c6dc17aab88a
     1.1 --- a/src/HOL/TLA/TLA.thy	Fri Nov 09 00:06:15 2001 +0100
     1.2 +++ b/src/HOL/TLA/TLA.thy	Fri Nov 09 00:09:47 2001 +0100
     1.3 @@ -55,7 +55,7 @@
     1.4    "sigma |= EEX x. F"    <= "_EEx x F sigma"
     1.5    "sigma |= AALL x. F"    <= "_AAll x F sigma"
     1.6  
     1.7 -syntax (symbols)
     1.8 +syntax (xsymbols)
     1.9    "_Box"     :: lift => lift                        ("(\\<box>_)" [40] 40)
    1.10    "_Dmd"     :: lift => lift                        ("(\\<diamond>_)" [40] 40)
    1.11    "_leadsto" :: [lift,lift] => lift                 ("(_ \\<leadsto> _)" [23,22] 22)