diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/UNITY/Simple/Lift.thy
--- a/src/HOL/UNITY/Simple/Lift.thy	Mon Oct 22 11:01:30 2001 +0200
+++ b/src/HOL/UNITY/Simple/Lift.thy	Mon Oct 22 11:54:22 2001 +0200
@@ -87,25 +87,25 @@
   req_up :: "(state*state) set"
     "req_up ==
          {(s,s'). s' = s (|stop  :=False,
-			   floor := floor s + Numeral1,
+			   floor := floor s + 1,
 			   up    := True|)
 		       & s : (ready Int goingup)}"
 
   req_down :: "(state*state) set"
     "req_down ==
          {(s,s'). s' = s (|stop  :=False,
-			   floor := floor s - Numeral1,
+			   floor := floor s - 1,
 			   up    := False|)
 		       & s : (ready Int goingdown)}"
 
   move_up :: "(state*state) set"
     "move_up ==
-         {(s,s'). s' = s (|floor := floor s + Numeral1|)
+         {(s,s'). s' = s (|floor := floor s + 1|)
 		       & ~ stop s & up s & floor s ~: req s}"
 
   move_down :: "(state*state) set"
     "move_down ==
-         {(s,s'). s' = s (|floor := floor s - Numeral1|)
+         {(s,s'). s' = s (|floor := floor s - 1|)
 		       & ~ stop s & ~ up s & floor s ~: req s}"
 
   (*This action is omitted from prior treatments, which therefore are
@@ -156,7 +156,7 @@
              else
              if n < floor s then (if up s then (Max - floor s) + (Max-n)
 		                  else floor s - n)
-             else Numeral0"
+             else 0"
 
 locale floor =
   fixes