# HG changeset patch
# User wenzelm
# Date 876305759 -7200
# Node ID 8489375c6198684e9857ed7d9760cae00c9914e9
# Parent  82a99b090d9de864fb8a3ecf6742dc87f464bb06
symbols syntax;

diff -r 82a99b090d9d -r 8489375c6198 src/HOL/TLA/Intensional.thy
--- a/src/HOL/TLA/Intensional.thy	Wed Oct 08 11:50:33 1997 +0200
+++ b/src/HOL/TLA/Intensional.thy	Wed Oct 08 12:15:59 1997 +0200
@@ -84,6 +84,10 @@
 
   "w |= A"              => "A(w)"
 
+syntax (symbols)
+  holdsAt  :: "['w::world, 'w form] => bool"   ("(_ \\<Turnstile> _)" [100,9] 8)
+
+
 rules
   inteq_reflection   "(x .= y) ==> (x == y)"
 
@@ -96,6 +100,5 @@
 
   unl_Rall    "(RALL x. A(x)) w == ALL x. (w |= A(x))"
   unl_Rex     "(REX x. A(x)) w == EX x. (w |= A(x))"
+
 end
-
-ML
diff -r 82a99b090d9d -r 8489375c6198 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