src/HOL/UNITY/Lift.thy
changeset 5596 b29d18d8c4d2
parent 5584 aad639e56d4e
child 5931 325300576da7
     1.1 --- a/src/HOL/UNITY/Lift.thy	Thu Oct 01 18:27:55 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Lift.thy	Thu Oct 01 18:28:18 1998 +0200
     1.3 @@ -116,10 +116,10 @@
     1.4  
     1.5    Lprg :: state program
     1.6      (*for the moment, we OMIT button_press*)
     1.7 -    "Lprg == (|Init = {s. floor s = Min & ~ up s & move s & stop s &
     1.8 +    "Lprg == mk_program ({s. floor s = Min & ~ up s & move s & stop s &
     1.9  		          ~ open s & req s = {}},
    1.10 -	       Acts0 = {request_act, open_act, close_act,
    1.11 -		        req_up, req_down, move_up, move_down}|)"
    1.12 +			 {request_act, open_act, close_act,
    1.13 +			  req_up, req_down, move_up, move_down})"
    1.14  
    1.15  
    1.16    (** Invariants **)