src/HOL/TLA/Intensional.thy
changeset 3808 8489375c6198
parent 3807 82a99b090d9d
child 6255 db63752140c7
     1.1 --- a/src/HOL/TLA/Intensional.thy	Wed Oct 08 11:50:33 1997 +0200
     1.2 +++ b/src/HOL/TLA/Intensional.thy	Wed Oct 08 12:15:59 1997 +0200
     1.3 @@ -84,6 +84,10 @@
     1.4  
     1.5    "w |= A"              => "A(w)"
     1.6  
     1.7 +syntax (symbols)
     1.8 +  holdsAt  :: "['w::world, 'w form] => bool"   ("(_ \\<Turnstile> _)" [100,9] 8)
     1.9 +
    1.10 +
    1.11  rules
    1.12    inteq_reflection   "(x .= y) ==> (x == y)"
    1.13  
    1.14 @@ -96,6 +100,5 @@
    1.15  
    1.16    unl_Rall    "(RALL x. A(x)) w == ALL x. (w |= A(x))"
    1.17    unl_Rex     "(REX x. A(x)) w == EX x. (w |= A(x))"
    1.18 +
    1.19  end
    1.20 -
    1.21 -ML