more antiquotations;
authorwenzelm
Fri Apr 08 14:05:31 2011 +0200 (2011-04-08)
changeset 4228624075ad39ca2
parent 42285 8d91a85b6d91
child 42287 d98eb048a2e4
more antiquotations;
src/HOL/Hoare_Parallel/OG_Syntax.thy
     1.1 --- a/src/HOL/Hoare_Parallel/OG_Syntax.thy	Fri Apr 08 13:59:28 2011 +0200
     1.2 +++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy	Fri Apr 08 14:05:31 2011 +0200
     1.3 @@ -115,13 +115,13 @@
     1.4    in
     1.5     [(@{const_syntax Collect}, assert_tr'),
     1.6      (@{const_syntax Basic}, assign_tr'),
     1.7 -    (@{const_syntax Cond}, bexp_tr' "_Cond"),
     1.8 -    (@{const_syntax While}, bexp_tr' "_While_inv"),
     1.9 +    (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}),
    1.10 +    (@{const_syntax While}, bexp_tr' @{syntax_const "_While_inv"}),
    1.11      (@{const_syntax AnnBasic}, annassign_tr'),
    1.12 -    (@{const_syntax AnnWhile}, annbexp_tr' "_AnnWhile"),
    1.13 -    (@{const_syntax AnnAwait}, annbexp_tr' "_AnnAwait"),
    1.14 -    (@{const_syntax AnnCond1}, annbexp_tr' "_AnnCond1"),
    1.15 -    (@{const_syntax AnnCond2}, annbexp_tr' "_AnnCond2")]
    1.16 +    (@{const_syntax AnnWhile}, annbexp_tr' @{syntax_const "_AnnWhile"}),
    1.17 +    (@{const_syntax AnnAwait}, annbexp_tr' @{syntax_const "_AnnAwait"}),
    1.18 +    (@{const_syntax AnnCond1}, annbexp_tr' @{syntax_const "_AnnCond1"}),
    1.19 +    (@{const_syntax AnnCond2}, annbexp_tr' @{syntax_const "_AnnCond2"})]
    1.20    end;
    1.21  *}
    1.22