| changeset 1789 | aade046ec6d5 |
| parent 1700 | afd3b60660db |
| child 4897 | be11be0b6ea1 |
| 1788:ca62fab4ce92 | 1789:aade046ec6d5 |
|---|---|
16 |
16 |
17 constdefs assign :: [state,val,loc] => state ("_[_'/_]" [95,0,0] 95) |
17 constdefs assign :: [state,val,loc] => state ("_[_'/_]" [95,0,0] 95) |
18 "s[m/x] == (%y. if y=x then m else s y)" |
18 "s[m/x] == (%y. if y=x then m else s y)" |
19 |
19 |
20 |
20 |
21 inductive "evalc" |
21 inductive evalc |
22 intrs |
22 intrs |
23 Skip "<SKIP,s> -c-> s" |
23 Skip "<SKIP,s> -c-> s" |
24 |
24 |
25 Assign "<x := a,s> -c-> s[a(s)/x]" |
25 Assign "<x := a,s> -c-> s[a(s)/x]" |
26 |
26 |