diff -r 0d2b31e1ea1b -r bafe45732b10 src/HOL/ex/Multiquote.thy
--- 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