# HG changeset patch # User wenzelm # Date 1729453718 -7200 # Node ID 7c2745efec69915b5d25dd55450c60c3c5b8acd3 # Parent d1170873976e045bd24b90d386878439ac79d099 clarified concrete vs. abstract syntax; diff -r d1170873976e -r 7c2745efec69 src/HOL/ex/Antiquote.thy --- a/src/HOL/ex/Antiquote.thy Sun Oct 20 20:32:53 2024 +0200 +++ b/src/HOL/ex/Antiquote.thy Sun Oct 20 21:48:38 2024 +0200 @@ -10,22 +10,20 @@ text \A simple example on quote / antiquote in higher-order abstract syntax.\ -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" syntax "_Expr" :: "'a \ 'a" (\EXPR _\ [1000] 999) + "_Var" :: "'a \ ('a \ nat) \ nat" (\VAR _\ [1000] 999) parse_translation \[Syntax_Trans.quote_antiquote_tr - \<^syntax_const>\_Expr\ \<^const_syntax>\var\ \<^const_syntax>\Expr\]\ + \<^syntax_const>\_Expr\ \<^syntax_const>\_Var\ \<^const_syntax>\Expr\]\ print_translation \[Syntax_Trans.quote_antiquote_tr' - \<^syntax_const>\_Expr\ \<^const_syntax>\var\ \<^const_syntax>\Expr\]\ + \<^syntax_const>\_Expr\ \<^syntax_const>\_Var\ \<^const_syntax>\Expr\]\ term "EXPR (a + b + c)" term "EXPR (a + b + c + VAR x + VAR y + 1)"