equal
deleted
inserted
replaced
21 "_fassign" :: "'a ref => id => 'v => 's com" |
21 "_fassign" :: "'a ref => id => 'v => 's com" |
22 ("(2_^._ :=/ _)" [70,1000,65] 61) |
22 ("(2_^._ :=/ _)" [70,1000,65] 61) |
23 "_faccess" :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v" |
23 "_faccess" :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v" |
24 ("_^._" [65,1000] 65) |
24 ("_^._" [65,1000] 65) |
25 translations |
25 translations |
26 "_refupdate f r v" == "f(CONST addr r := v)" |
26 "_refupdate f r v" == "f(CONST addr r := v)" |
27 "p^.f := e" => "(p \<noteq> CONST Null) \<rightarrow> (f := _refupdate f p e)" |
27 "p^.f := e" => "(p \<noteq> CONST Null) \<rightarrow> (f := _refupdate f p e)" |
28 "p^.f" => "f(CONST addr p)" |
28 "p^.f" => "f(CONST addr p)" |
29 |
29 |
30 |
30 |
31 declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp] |
31 declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp] |
32 |
32 |
33 |
33 |