equal
deleted
inserted
replaced
41 |
41 |
42 syntax |
42 syntax |
43 "_prg_scheme" :: "['a, 'a, 'a, 'a] \<Rightarrow> prgs" ("SCHEME [_ \<le> _ < _] _" [0,0,0,60] 57) |
43 "_prg_scheme" :: "['a, 'a, 'a, 'a] \<Rightarrow> prgs" ("SCHEME [_ \<le> _ < _] _" [0,0,0,60] 57) |
44 |
44 |
45 translations |
45 translations |
46 "_prg_scheme j i k c" \<rightleftharpoons> "(map (\<lambda>i. c) [j..<k])" |
46 "_prg_scheme j i k c" \<rightleftharpoons> "(CONST map (\<lambda>i. c) [j..<k])" |
47 |
47 |
48 text {* Translations for variables before and after a transition: *} |
48 text {* Translations for variables before and after a transition: *} |
49 |
49 |
50 syntax |
50 syntax |
51 "_before" :: "id \<Rightarrow> 'a" ("\<ordmasculine>_") |
51 "_before" :: "id \<Rightarrow> 'a" ("\<ordmasculine>_") |