src/HOL/UNITY/Lift.thy
changeset 5931 325300576da7
parent 5596 b29d18d8c4d2
child 6012 1894bfc4aee9
     1.1 --- a/src/HOL/UNITY/Lift.thy	Wed Nov 18 11:12:29 1998 +0100
     1.2 +++ b/src/HOL/UNITY/Lift.thy	Wed Nov 18 15:10:46 1998 +0100
     1.3 @@ -36,10 +36,10 @@
     1.4      "queueing == above Un below"
     1.5  
     1.6    goingup :: state set
     1.7 -    "goingup   == above Int  ({s. up s}  Un Compl below)"
     1.8 +    "goingup   == above Int  ({s. up s}  Un -below)"
     1.9  
    1.10    goingdown :: state set
    1.11 -    "goingdown == below Int ({s. ~ up s} Un Compl above)"
    1.12 +    "goingdown == below Int ({s. ~ up s} Un -above)"
    1.13  
    1.14    ready :: state set
    1.15      "ready == {s. stop s & ~ open s & move s}"