equal
deleted
inserted
replaced
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 |
5 |
6 Simple quote / antiquote example. |
6 Simple quote / antiquote example. |
7 *) |
7 *) |
|
8 |
|
9 header {* Antiquotations *} |
8 |
10 |
9 theory Antiquote = Main: |
11 theory Antiquote = Main: |
10 |
12 |
11 syntax |
13 syntax |
12 "_Expr" :: "'a => 'a" ("EXPR _" [1000] 999) |
14 "_Expr" :: "'a => 'a" ("EXPR _" [1000] 999) |
23 |
25 |
24 term "EXPR (a + b + c)" |
26 term "EXPR (a + b + c)" |
25 term "EXPR (a + b + c + VAR x + VAR y + 1)" |
27 term "EXPR (a + b + c + VAR x + VAR y + 1)" |
26 term "EXPR (VAR (f w) + VAR x)" |
28 term "EXPR (VAR (f w) + VAR x)" |
27 |
29 |
28 term "Expr (%env. env x)" (*improper*) |
30 term "Expr (\<lambda>env. env x)" (*improper*) |
29 term "Expr (%env. f env)" |
31 term "Expr (\<lambda>env. f env)" |
30 term "Expr (%env. f env + env x)" (*improper*) |
32 term "Expr (\<lambda>env. f env + env x)" (*improper*) |
31 term "Expr (%env. f env y z)" |
33 term "Expr (\<lambda>env. f env y z)" |
32 term "Expr (%env. f env + g y env)" |
34 term "Expr (\<lambda>env. f env + g y env)" |
33 term "Expr (%env. f env + g env y + h a env z)" |
35 term "Expr (\<lambda>env. f env + g env y + h a env z)" |
34 |
36 |
35 end |
37 end |
36 |
38 |