--- a/src/HOL/ex/Multiquote.thy Thu Jul 13 11:41:06 2000 +0200
+++ b/src/HOL/ex/Multiquote.thy Thu Jul 13 11:41:40 2000 +0200
@@ -1,16 +1,17 @@
(* Title: HOL/ex/Multiquote.thy
ID: $Id$
Author: Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Multiple nested quotations and anti-quotations -- basically a
generalized version of de-Bruijn representation.
*)
-theory Multiquote = Main:;
+theory Multiquote = Main:
syntax
"_quote" :: "'b => ('a => 'b)" (".'(_')." [0] 1000)
- "_antiquote" :: "('a => 'b) => 'b" ("`_" [1000] 1000);
+ "_antiquote" :: "('a => 'b) => 'b" ("`_" [1000] 1000)
parse_translation {*
let
@@ -28,18 +29,18 @@
fun quote_tr [t] = Abs ("s", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
| quote_tr ts = raise TERM ("quote_tr", ts);
in [("_quote", quote_tr)] end
-*};
+*}
-text {* basic examples *};
-term ".(a + b + c).";
-term ".(a + b + c + `x + `y + 1).";
-term ".(`(f w) + `x).";
-term ".(f `x `y z).";
+text {* basic examples *}
+term ".(a + b + c)."
+term ".(a + b + c + `x + `y + 1)."
+term ".(`(f w) + `x)."
+term ".(f `x `y z)."
-text {* advanced examples *};
-term ".(.(` `x + `y).).";
-term ".(.(` `x + `y). o `f).";
-term ".(`(f o `g)).";
-term ".(.( ` `(f o `g) ).).";
+text {* advanced examples *}
+term ".(.(` `x + `y).)."
+term ".(.(` `x + `y). o `f)."
+term ".(`(f o `g))."
+term ".(.( ` `(f o `g) ).)."
-end;
+end