equal
deleted
inserted
replaced
19 syntax |
19 syntax |
20 "_Expr" :: "'a \<Rightarrow> 'a" ("EXPR _" [1000] 999) |
20 "_Expr" :: "'a \<Rightarrow> 'a" ("EXPR _" [1000] 999) |
21 |
21 |
22 parse_translation |
22 parse_translation |
23 \<open>[Syntax_Trans.quote_antiquote_tr |
23 \<open>[Syntax_Trans.quote_antiquote_tr |
24 @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]\<close> |
24 \<^syntax_const>\<open>_Expr\<close> \<^const_syntax>\<open>var\<close> \<^const_syntax>\<open>Expr\<close>]\<close> |
25 |
25 |
26 print_translation |
26 print_translation |
27 \<open>[Syntax_Trans.quote_antiquote_tr' |
27 \<open>[Syntax_Trans.quote_antiquote_tr' |
28 @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]\<close> |
28 \<^syntax_const>\<open>_Expr\<close> \<^const_syntax>\<open>var\<close> \<^const_syntax>\<open>Expr\<close>]\<close> |
29 |
29 |
30 term "EXPR (a + b + c)" |
30 term "EXPR (a + b + c)" |
31 term "EXPR (a + b + c + VAR x + VAR y + 1)" |
31 term "EXPR (a + b + c + VAR x + VAR y + 1)" |
32 term "EXPR (VAR (f w) + VAR x)" |
32 term "EXPR (VAR (f w) + VAR x)" |
33 |
33 |