| changeset 34940 | 3e80eab831a1 |
| parent 32621 | a073cb249a06 |
| child 35107 | bdca9f765ee4 |
--- a/src/HOL/Hoare_Parallel/OG_Syntax.thy Sat Jan 16 17:15:27 2010 +0100 +++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy Sat Jan 16 17:15:27 2010 +0100 @@ -72,7 +72,7 @@ "_prgs c q ps" \<rightleftharpoons> "(Some c, q) # ps" "_PAR ps" \<rightleftharpoons> "Parallel ps" - "_prg_scheme j i k c q" \<rightleftharpoons> "map (\<lambda>i. (Some c, q)) [j..<k]" + "_prg_scheme j i k c q" \<rightleftharpoons> "CONST map (\<lambda>i. (Some c, q)) [j..<k]" print_translation {* let