--- a/src/HOL/UNITY/Lift.thy Thu Oct 01 18:27:55 1998 +0200
+++ b/src/HOL/UNITY/Lift.thy Thu Oct 01 18:28:18 1998 +0200
@@ -116,10 +116,10 @@
Lprg :: state program
(*for the moment, we OMIT button_press*)
- "Lprg == (|Init = {s. floor s = Min & ~ up s & move s & stop s &
+ "Lprg == mk_program ({s. floor s = Min & ~ up s & move s & stop s &
~ open s & req s = {}},
- Acts0 = {request_act, open_act, close_act,
- req_up, req_down, move_up, move_down}|)"
+ {request_act, open_act, close_act,
+ req_up, req_down, move_up, move_down})"
(** Invariants **)