--- a/src/HOL/ex/Antiquote.thy Thu Sep 27 15:42:01 2001 +0200
+++ b/src/HOL/ex/Antiquote.thy Thu Sep 27 15:42:08 2001 +0200
@@ -2,14 +2,17 @@
ID: $Id$
Author: Markus Wenzel, TU Muenchen
License: GPL (GNU GENERAL PUBLIC LICENSE)
-
-Simple quote / antiquote example.
*)
header {* Antiquotations *}
theory Antiquote = Main:
+text {*
+ A simple example on quote / antiquote in higher-order abstract
+ syntax.
+*}
+
syntax
"_Expr" :: "'a => 'a" ("EXPR _" [1000] 999)
@@ -35,4 +38,3 @@
term "Expr (\<lambda>env. f env + g env y + h a env z)"
end
-