no longer declare .psimps rules as [simp].
This regularly caused confusion (e.g., they show up in simp traces
when the regular simp rules are disabled). In the few places where the
rules are used, explicitly mentioning them actually clarifies the
proof text.
(* Title: HOL/ex/Antiquote.thy
Author: Markus Wenzel, TU Muenchen
*)
header {* Antiquotations *}
theory Antiquote
imports Main
begin
text {*
A simple example on quote / antiquote in higher-order abstract
syntax.
*}
syntax
"_Expr" :: "'a => 'a" ("EXPR _" [1000] 999)
definition
var :: "'a => ('a => nat) => nat" ("VAR _" [1000] 999)
where "var x env = env x"
definition
Expr :: "(('a => nat) => nat) => ('a => nat) => nat"
where "Expr exp env = exp env"
parse_translation {*
[Syntax.quote_antiquote_tr @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
*}
print_translation {*
[Syntax.quote_antiquote_tr' @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
*}
term "EXPR (a + b + c)"
term "EXPR (a + b + c + VAR x + VAR y + 1)"
term "EXPR (VAR (f w) + VAR x)"
term "Expr (\<lambda>env. env x)" -- {* improper *}
term "Expr (\<lambda>env. f env)"
term "Expr (\<lambda>env. f env + env x)" -- {* improper *}
term "Expr (\<lambda>env. f env y z)"
term "Expr (\<lambda>env. f env + g y env)"
term "Expr (\<lambda>env. f env + g env y + h a env z)"
end