src/HOL/Hoare_Parallel/OG_Syntax.thy
changeset 34940 3e80eab831a1
parent 32621 a073cb249a06
child 35107 bdca9f765ee4
equal deleted inserted replaced
34939:44294cfecb1d 34940:3e80eab831a1
    70 translations
    70 translations
    71   "_prg c q" \<rightleftharpoons> "[(Some c, q)]"
    71   "_prg c q" \<rightleftharpoons> "[(Some c, q)]"
    72   "_prgs c q ps" \<rightleftharpoons> "(Some c, q) # ps"
    72   "_prgs c q ps" \<rightleftharpoons> "(Some c, q) # ps"
    73   "_PAR ps" \<rightleftharpoons> "Parallel ps"
    73   "_PAR ps" \<rightleftharpoons> "Parallel ps"
    74 
    74 
    75   "_prg_scheme j i k c q" \<rightleftharpoons> "map (\<lambda>i. (Some c, q)) [j..<k]"
    75   "_prg_scheme j i k c q" \<rightleftharpoons> "CONST map (\<lambda>i. (Some c, q)) [j..<k]"
    76 
    76 
    77 print_translation {*
    77 print_translation {*
    78   let
    78   let
    79     fun quote_tr' f (t :: ts) =
    79     fun quote_tr' f (t :: ts) =
    80           Term.list_comb (f $ Syntax.quote_tr' "_antiquote" t, ts)
    80           Term.list_comb (f $ Syntax.quote_tr' "_antiquote" t, ts)