src/HOL/UNITY/Simple/Lift.thy
changeset 11701 3d51fbf81c17
parent 11195 65ede8dfe304
child 11868 56db9f3a6b3e
     1.1 --- a/src/HOL/UNITY/Simple/Lift.thy	Fri Oct 05 21:50:37 2001 +0200
     1.2 +++ b/src/HOL/UNITY/Simple/Lift.thy	Fri Oct 05 21:52:39 2001 +0200
     1.3 @@ -87,25 +87,25 @@
     1.4    req_up :: "(state*state) set"
     1.5      "req_up ==
     1.6           {(s,s'). s' = s (|stop  :=False,
     1.7 -			   floor := floor s + #1,
     1.8 +			   floor := floor s + Numeral1,
     1.9  			   up    := True|)
    1.10  		       & s : (ready Int goingup)}"
    1.11  
    1.12    req_down :: "(state*state) set"
    1.13      "req_down ==
    1.14           {(s,s'). s' = s (|stop  :=False,
    1.15 -			   floor := floor s - #1,
    1.16 +			   floor := floor s - Numeral1,
    1.17  			   up    := False|)
    1.18  		       & s : (ready Int goingdown)}"
    1.19  
    1.20    move_up :: "(state*state) set"
    1.21      "move_up ==
    1.22 -         {(s,s'). s' = s (|floor := floor s + #1|)
    1.23 +         {(s,s'). s' = s (|floor := floor s + Numeral1|)
    1.24  		       & ~ stop s & up s & floor s ~: req s}"
    1.25  
    1.26    move_down :: "(state*state) set"
    1.27      "move_down ==
    1.28 -         {(s,s'). s' = s (|floor := floor s - #1|)
    1.29 +         {(s,s'). s' = s (|floor := floor s - Numeral1|)
    1.30  		       & ~ stop s & ~ up s & floor s ~: req s}"
    1.31  
    1.32    (*This action is omitted from prior treatments, which therefore are
    1.33 @@ -156,7 +156,7 @@
    1.34               else
    1.35               if n < floor s then (if up s then (Max - floor s) + (Max-n)
    1.36  		                  else floor s - n)
    1.37 -             else #0"
    1.38 +             else Numeral0"
    1.39  
    1.40  locale floor =
    1.41    fixes