113 |
113 |
114 fun Parallel_tr' ts = Syntax.const @{syntax_const "_PAR"} $ Parallel_PAR ts; |
114 fun Parallel_tr' ts = Syntax.const @{syntax_const "_PAR"} $ Parallel_PAR ts; |
115 in |
115 in |
116 [(@{const_syntax Collect}, assert_tr'), |
116 [(@{const_syntax Collect}, assert_tr'), |
117 (@{const_syntax Basic}, assign_tr'), |
117 (@{const_syntax Basic}, assign_tr'), |
118 (@{const_syntax Cond}, bexp_tr' "_Cond"), |
118 (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}), |
119 (@{const_syntax While}, bexp_tr' "_While_inv"), |
119 (@{const_syntax While}, bexp_tr' @{syntax_const "_While_inv"}), |
120 (@{const_syntax AnnBasic}, annassign_tr'), |
120 (@{const_syntax AnnBasic}, annassign_tr'), |
121 (@{const_syntax AnnWhile}, annbexp_tr' "_AnnWhile"), |
121 (@{const_syntax AnnWhile}, annbexp_tr' @{syntax_const "_AnnWhile"}), |
122 (@{const_syntax AnnAwait}, annbexp_tr' "_AnnAwait"), |
122 (@{const_syntax AnnAwait}, annbexp_tr' @{syntax_const "_AnnAwait"}), |
123 (@{const_syntax AnnCond1}, annbexp_tr' "_AnnCond1"), |
123 (@{const_syntax AnnCond1}, annbexp_tr' @{syntax_const "_AnnCond1"}), |
124 (@{const_syntax AnnCond2}, annbexp_tr' "_AnnCond2")] |
124 (@{const_syntax AnnCond2}, annbexp_tr' @{syntax_const "_AnnCond2"})] |
125 end; |
125 end; |
126 *} |
126 *} |
127 |
127 |
128 end |
128 end |