equal
deleted
inserted
replaced
23 definition |
23 definition |
24 Expr :: "(('a => nat) => nat) => ('a => nat) => nat" |
24 Expr :: "(('a => nat) => nat) => ('a => nat) => nat" |
25 where "Expr exp env = exp env" |
25 where "Expr exp env = exp env" |
26 |
26 |
27 parse_translation {* |
27 parse_translation {* |
28 [Syntax.quote_antiquote_tr @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}] |
28 [Syntax_Trans.quote_antiquote_tr |
|
29 @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}] |
29 *} |
30 *} |
30 |
31 |
31 print_translation {* |
32 print_translation {* |
32 [Syntax.quote_antiquote_tr' @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}] |
33 [Syntax_Trans.quote_antiquote_tr' |
|
34 @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}] |
33 *} |
35 *} |
34 |
36 |
35 term "EXPR (a + b + c)" |
37 term "EXPR (a + b + c)" |
36 term "EXPR (a + b + c + VAR x + VAR y + 1)" |
38 term "EXPR (a + b + c + VAR x + VAR y + 1)" |
37 term "EXPR (VAR (f w) + VAR x)" |
39 term "EXPR (VAR (f w) + VAR x)" |