--- a/src/HOL/TLA/TLA.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/TLA/TLA.thy Wed Apr 14 14:13:05 2004 +0200
@@ -62,6 +62,10 @@
"_EEx" :: [idts, lift] => lift ("(3\\<exists>\\<exists> _./ _)" [0,10] 10)
"_AAll" :: [idts, lift] => lift ("(3\\<forall>\\<forall> _./ _)" [0,10] 10)
+syntax (HTML output)
+ "_EEx" :: [idts, lift] => lift ("(3\\<exists>\\<exists> _./ _)" [0,10] 10)
+ "_AAll" :: [idts, lift] => lift ("(3\\<forall>\\<forall> _./ _)" [0,10] 10)
+
rules
(* Definitions of derived operators *)
dmd_def "TEMP <>F == TEMP ~[]~F"