src/HOL/Hoare_Parallel/RG_Syntax.thy
changeset 34940 3e80eab831a1
parent 32621 a073cb249a06
child 35107 bdca9f765ee4
     1.1 --- a/src/HOL/Hoare_Parallel/RG_Syntax.thy	Sat Jan 16 17:15:27 2010 +0100
     1.2 +++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy	Sat Jan 16 17:15:27 2010 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4    "_prg_scheme" :: "['a, 'a, 'a, 'a] \<Rightarrow> prgs"  ("SCHEME [_ \<le> _ < _] _" [0,0,0,60] 57)
     1.5  
     1.6  translations
     1.7 -  "_prg_scheme j i k c" \<rightleftharpoons> "(map (\<lambda>i. c) [j..<k])"
     1.8 +  "_prg_scheme j i k c" \<rightleftharpoons> "(CONST map (\<lambda>i. c) [j..<k])"
     1.9  
    1.10  text {* Translations for variables before and after a transition: *}
    1.11