equal
deleted
inserted
replaced
26 | Assign loc aexp ("_ :== _ " 60) |
26 | Assign loc aexp ("_ :== _ " 60) |
27 | Semi com com ("_; _" [60, 60] 10) |
27 | Semi com com ("_; _" [60, 60] 10) |
28 | Cond bexp com com ("IF _ THEN _ ELSE _" 60) |
28 | Cond bexp com com ("IF _ THEN _ ELSE _" 60) |
29 | While bexp com ("WHILE _ DO _" 60) |
29 | While bexp com ("WHILE _ DO _" 60) |
30 |
30 |
31 syntax (latex) |
31 notation (latex) |
32 SKIP :: com ("\<SKIP>") |
32 SKIP ("\<SKIP>") and |
33 Cond :: "bexp \<Rightarrow> com \<Rightarrow> com \<Rightarrow> com" ("\<IF> _ \<THEN> _ \<ELSE> _" 60) |
33 Cond ("\<IF> _ \<THEN> _ \<ELSE> _" 60) and |
34 While :: "bexp \<Rightarrow> com \<Rightarrow> com" ("\<WHILE> _ \<DO> _" 60) |
34 While ("\<WHILE> _ \<DO> _" 60) |
35 |
35 |
36 end |
36 end |