src/HOL/TLA/TLA.thy
changeset 14565 c6dc17aab88a
parent 12114 a8e860c86252
child 17309 c43ed29bd197
     1.1 --- a/src/HOL/TLA/TLA.thy	Wed Apr 14 13:28:46 2004 +0200
     1.2 +++ b/src/HOL/TLA/TLA.thy	Wed Apr 14 14:13:05 2004 +0200
     1.3 @@ -62,6 +62,10 @@
     1.4    "_EEx"     :: [idts, lift] => lift                ("(3\\<exists>\\<exists> _./ _)" [0,10] 10)
     1.5    "_AAll"    :: [idts, lift] => lift                ("(3\\<forall>\\<forall> _./ _)" [0,10] 10)
     1.6  
     1.7 +syntax (HTML output)
     1.8 +  "_EEx"     :: [idts, lift] => lift                ("(3\\<exists>\\<exists> _./ _)" [0,10] 10)
     1.9 +  "_AAll"    :: [idts, lift] => lift                ("(3\\<forall>\\<forall> _./ _)" [0,10] 10)
    1.10 +
    1.11  rules
    1.12    (* Definitions of derived operators *)
    1.13    dmd_def      "TEMP <>F  ==  TEMP ~[]~F"