src/HOL/ex/Antiquote.thy

revised for new treatment of integers

(*  Title:      HOL/ex/Antiquote.thy
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

Simple quote / antiquote example.
*)

Antiquote = Arith +

syntax
  "_Expr" :: "'a => 'a"				("EXPR _" [1000] 999)

constdefs
  var :: "'a => ('a => nat) => nat"		("VAR _" [1000] 999)
  "var x env == env x"

  Expr :: "'a => 'a"
	(*"(('a => nat) => nat) => (('a => nat) => nat)"*)
  "Expr == (%x. x)"

end


ML

val parse_translation = [Syntax.quote_antiquote_tr "_Expr" "var" "Expr"];
val print_translation = [Syntax.quote_antiquote_tr' "_Expr" "var" "Expr"];