src/HOL/ex/Multiquote.thy
changeset 11586 d8a7f6318457
parent 11020 646c929b6293
child 11823 5a3fcd84e55e
     1.1 --- a/src/HOL/ex/Multiquote.thy	Thu Sep 27 15:42:01 2001 +0200
     1.2 +++ b/src/HOL/ex/Multiquote.thy	Thu Sep 27 15:42:08 2001 +0200
     1.3 @@ -2,15 +2,17 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.7 -
     1.8 -Multiple nested quotations and anti-quotations -- basically a
     1.9 -generalized version of de-Bruijn representation.
    1.10  *)
    1.11  
    1.12  header {* Multiple nested quotations and anti-quotations *}
    1.13  
    1.14  theory Multiquote = Main:
    1.15  
    1.16 +text {*
    1.17 +  Multiple nested quotations and anti-quotations -- basically a
    1.18 +  generalized version of de-Bruijn representation.
    1.19 +*}
    1.20 +
    1.21  syntax
    1.22    "_quote" :: "'b => ('a => 'b)"	     (".'(_')." [0] 1000)
    1.23    "_antiquote" :: "('a => 'b) => 'b"         ("\<acute>_" [1000] 1000)