src/HOL/TLA/TLA.thy

--- a/src/HOL/TLA/TLA.thy	Wed Oct 08 11:50:33 1997 +0200
+++ b/src/HOL/TLA/TLA.thy	Wed Oct 08 12:15:59 1997 +0200
@@ -45,6 +45,10 @@
   "sigma |= WF(A)_v"      == "WF A v sigma"
   "sigma |= SF(A)_v"      == "SF A v sigma"
 
+syntax (symbols)
+  Box        :: "('w::world) form => temporal"      ("(\\<box>(_))" [40] 40)
+  Dmd        :: "('w::world) form => temporal"      ("(\\<diamond>(_))" [40] 40)
+
 rules
   dmd_def    "(<>F) == .~[].~F"
   boxact_def "([](F::action)) == ([] Init F)"
@@ -81,5 +85,3 @@
 		 |] ==> G sigma"
 
 end
-
-ML