--- a/src/HOL/ex/Antiquote.thy Thu Mar 23 10:23:54 2000 +0100
+++ b/src/HOL/ex/Antiquote.thy Thu Mar 23 11:27:52 2000 +0100
@@ -5,23 +5,31 @@
Simple quote / antiquote example.
*)
-Antiquote = Arith +
+theory Antiquote = Main:;
syntax
- "_Expr" :: "'a => 'a" ("EXPR _" [1000] 999)
+ "_Expr" :: "'a => 'a" ("EXPR _" [1000] 999);
constdefs
var :: "'a => ('a => nat) => nat" ("VAR _" [1000] 999)
"var x env == env x"
- Expr :: "'a => 'a"
- (*"(('a => nat) => nat) => (('a => nat) => nat)"*)
- "Expr == (%x. x)"
+ Expr :: "(('a => nat) => nat) => ('a => nat) => nat"
+ "Expr exp env == exp env";
-end
+parse_translation {* [Syntax.quote_antiquote_tr "_Expr" "var" "Expr"] *};
+print_translation {* [Syntax.quote_antiquote_tr' "_Expr" "var" "Expr"] *};
+
+term "EXPR (a + b + c)";
+term "EXPR (a + b + c + VAR x + VAR y + 1)";
+term "EXPR (VAR (f w) + VAR x)";
-
-ML
+term "Expr (%env. env x)"; (*improper*)
+term "Expr (%env. f env)";
+term "Expr (%env. f env + env x)"; (*improper*)
+term "Expr (%env. f env y z)";
+term "Expr (%env. f env + g y env)";
+term "Expr (%env. f env + g env y + h a env z)";
-val parse_translation = [Syntax.quote_antiquote_tr "_Expr" "var" "Expr"];
-val print_translation = [Syntax.quote_antiquote_tr' "_Expr" "var" "Expr"];
+end;
+