equal
deleted
inserted
replaced
15 consts |
15 consts |
16 newlocs :: locals |
16 newlocs :: locals |
17 setlocs :: "state => locals => state" |
17 setlocs :: "state => locals => state" |
18 getlocs :: "state => locals" |
18 getlocs :: "state => locals" |
19 update :: "state => vname => val => state" ("_/[_/::=/_]" [900,0,0] 900) |
19 update :: "state => vname => val => state" ("_/[_/::=/_]" [900,0,0] 900) |
20 syntax (* IN Natural.thy *) |
20 |
21 loc :: "state => locals" ("_<_>" [75,0] 75) |
21 abbreviation |
22 translations |
22 loc :: "state => locals" ("_<_>" [75,0] 75) where |
23 "s<X>" == "getlocs s X" |
23 "s<X> == getlocs s X" |
24 |
24 |
25 inductive |
25 inductive |
26 evalc :: "[com,state, state] => bool" ("<_,_>/ -c-> _" [0,0, 51] 51) |
26 evalc :: "[com,state, state] => bool" ("<_,_>/ -c-> _" [0,0, 51] 51) |
27 where |
27 where |
28 Skip: "<SKIP,s> -c-> s" |
28 Skip: "<SKIP,s> -c-> s" |