src/HOL/TLA/TLA.thy

   "sigma |= WF(A)_v"     <= "_WF A v sigma"
   "sigma |= SF(A)_v"     <= "_SF A v sigma"
   "sigma |= EEX x. F"    <= "_EEx x F sigma"
   "sigma |= AALL x. F"    <= "_AAll x F sigma"
 
-syntax (symbols)
+syntax (xsymbols)
   "_Box"     :: lift => lift                        ("(\\<box>_)" [40] 40)
   "_Dmd"     :: lift => lift                        ("(\\<diamond>_)" [40] 40)
   "_leadsto" :: [lift,lift] => lift                 ("(_ \\<leadsto> _)" [23,22] 22)
   "_EEx"     :: [idts, lift] => lift                ("(3\\<exists>\\<exists> _./ _)" [0,10] 10)
   "_AAll"    :: [idts, lift] => lift                ("(3\\<forall>\\<forall> _./ _)" [0,10] 10)