src/HOL/Hoare_Parallel/Quote_Antiquote.thy
changeset 35107 bdca9f765ee4
parent 32621 a073cb249a06
child 35113 1a0c129bb2e0
     1.1 --- a/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Thu Feb 11 09:14:34 2010 +0100
     1.2 +++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Thu Feb 11 13:54:53 2010 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4    "_Assert"    :: "'a \<Rightarrow> 'a set"            ("(\<lbrace>_\<rbrace>)" [0] 1000)
     1.5  
     1.6  translations
     1.7 -  ".{b}." \<rightharpoonup> "Collect \<guillemotleft>b\<guillemotright>"
     1.8 +  ".{b}." \<rightharpoonup> "CONST Collect \<guillemotleft>b\<guillemotright>"
     1.9  
    1.10  parse_translation {*
    1.11    let