src/HOL/UNITY/Lift.thy
changeset 5584 aad639e56d4e
parent 5563 228b92552d1f
child 5596 b29d18d8c4d2
     1.1 --- a/src/HOL/UNITY/Lift.thy	Tue Sep 29 15:58:25 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Lift.thy	Tue Sep 29 15:58:47 1998 +0200
     1.3 @@ -118,8 +118,8 @@
     1.4      (*for the moment, we OMIT button_press*)
     1.5      "Lprg == (|Init = {s. floor s = Min & ~ up s & move s & stop s &
     1.6  		          ~ open s & req s = {}},
     1.7 -	       Acts = {id, request_act, open_act, close_act,
     1.8 -		       req_up, req_down, move_up, move_down}|)"
     1.9 +	       Acts0 = {request_act, open_act, close_act,
    1.10 +		        req_up, req_down, move_up, move_down}|)"
    1.11  
    1.12  
    1.13    (** Invariants **)