equal
deleted
inserted
replaced
8 syntax |
8 syntax |
9 "_Assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(\<acute>_ :=/ _)" [70, 65] 61) |
9 "_Assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(\<acute>_ :=/ _)" [70, 65] 61) |
10 "_AnnAssign" :: "'a assn \<Rightarrow> idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(_ \<acute>_ :=/ _)" [90,70,65] 61) |
10 "_AnnAssign" :: "'a assn \<Rightarrow> idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(_ \<acute>_ :=/ _)" [90,70,65] 61) |
11 |
11 |
12 translations |
12 translations |
13 "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (CONST K_record a))\<guillemotright>" |
13 "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (K_record a))\<guillemotright>" |
14 "r \<acute>\<spacespace>x := a" \<rightharpoonup> "AnnBasic r \<guillemotleft>\<acute>\<spacespace>(_update_name x (CONST K_record a))\<guillemotright>" |
14 "r \<acute>\<spacespace>x := a" \<rightharpoonup> "AnnBasic r \<guillemotleft>\<acute>\<spacespace>(_update_name x (K_record a))\<guillemotright>" |
15 |
15 |
16 syntax |
16 syntax |
17 "_AnnSkip" :: "'a assn \<Rightarrow> 'a ann_com" ("_//SKIP" [90] 63) |
17 "_AnnSkip" :: "'a assn \<Rightarrow> 'a ann_com" ("_//SKIP" [90] 63) |
18 "_AnnSeq" :: "'a ann_com \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com" ("_;;/ _" [60,61] 60) |
18 "_AnnSeq" :: "'a ann_com \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com" ("_;;/ _" [60,61] 60) |
19 |
19 |