--- 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
--- 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