--- a/src/HOL/ex/Antiquote.thy Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/ex/Antiquote.thy Sat Oct 17 14:43:18 2009 +0200
@@ -13,10 +13,10 @@
*}
syntax
- "_Expr" :: "'a => 'a" ("EXPR _" [1000] 999)
+ "_Expr" :: "'a => 'a" ("EXPR _" [1000] 999)
constdefs
- var :: "'a => ('a => nat) => nat" ("VAR _" [1000] 999)
+ var :: "'a => ('a => nat) => nat" ("VAR _" [1000] 999)
"var x env == env x"
Expr :: "(('a => nat) => nat) => ('a => nat) => nat"
@@ -29,9 +29,9 @@
term "EXPR (a + b + c + VAR x + VAR y + 1)"
term "EXPR (VAR (f w) + VAR x)"
-term "Expr (\<lambda>env. env x)" (*improper*)
+term "Expr (\<lambda>env. env x)" -- {* improper *}
term "Expr (\<lambda>env. f env)"
-term "Expr (\<lambda>env. f env + env x)" (*improper*)
+term "Expr (\<lambda>env. f env + env x)" -- {* improper *}
term "Expr (\<lambda>env. f env y z)"
term "Expr (\<lambda>env. f env + g y env)"
term "Expr (\<lambda>env. f env + g env y + h a env z)"