src/HOL/UNITY/Token.thy
changeset 5931 325300576da7
parent 5782 7559f116cb10
child 6536 281d44905cab
     1.1 --- a/src/HOL/UNITY/Token.thy	Wed Nov 18 11:12:29 1998 +0100
     1.2 +++ b/src/HOL/UNITY/Token.thy	Wed Nov 18 15:10:46 1998 +0100
     1.3 @@ -49,7 +49,7 @@
     1.4  
     1.5      TR4  "F : constrains (H i - HasTok i) (H i)"
     1.6  
     1.7 -    TR5  "F : constrains (HasTok i) (HasTok i Un Compl(E i))"
     1.8 +    TR5  "F : constrains (HasTok i) (HasTok i Un -(E i))"
     1.9  
    1.10      TR6  "F : leadsTo (H i Int HasTok i) (E i)"
    1.11