--- a/NEWS Sat Dec 09 18:05:34 2006 +0100
+++ b/NEWS Sat Dec 09 18:05:36 2006 +0100
@@ -45,13 +45,18 @@
*** Document preparation ***
-* Added antiquotation @{theory name} which prints the name $A$, after
-checking that it refers to a valid ancestor theory in the current
-context.
+* Added antiquotation @{theory name} which prints the given name,
+after checking that it refers to a valid ancestor theory in the
+current context.
* Added antiquotations @{ML_type text} and @{ML_struct text} which
check the given source text as ML type/structure, printing verbatim.
+* Added antiquotation @{abbrev "c args"} which prints the abbreviation
+"c args == rhs" given in the current context. (Any number of
+arguments on the LHS may be given.)
+
+
*** Pure ***
--- a/doc-src/IsarRef/syntax.tex Sat Dec 09 18:05:34 2006 +0100
+++ b/doc-src/IsarRef/syntax.tex Sat Dec 09 18:05:36 2006 +0100
@@ -435,6 +435,7 @@
prop & : & \isarantiq \\
term & : & \isarantiq \\
const & : & \isarantiq \\
+ abbrev & : & \isarantiq \\
typeof & : & \isarantiq \\
typ & : & \isarantiq \\
thm_style & : & \isarantiq \\
@@ -465,7 +466,7 @@
which are easier to read.
\indexisarant{theory}\indexisarant{thm}\indexisarant{prop}\indexisarant{term}\indexisarant{const}
-\indexisarant{typeof}\indexisarant{typ}\indexisarant{thm-style}
+\indexisarant{abbrev}\indexisarant{typeof}\indexisarant{typ}\indexisarant{thm-style}
\indexisarant{term-style}\indexisarant{text}\indexisarant{goals}
\indexisarant{subgoals}\indexisarant{prf}\indexisarant{full-prf}\indexisarant{ML}
\indexisarant{ML-type}\indexisarant{ML-struct}
@@ -480,6 +481,7 @@
'prop' options prop |
'term' options term |
'const' options term |
+ 'abbrev' options term |
'typeof' options term |
'typ' options type |
'thm\_style' options name thmref |
@@ -517,6 +519,9 @@
\item [$\at\{term~t\}$] prints a well-typed term $t$.
\item [$\at\{const~c\}$] prints a well-defined constant $c$.
+
+\item [$\at\{abbrev~c\,\vec x\}$] prints a constant abbreviation
+ $c\,\vec x \equiv rhs$ as defined in the current context.
\item [$\at\{typeof~t\}$] prints the type of a well-typed term $t$.
--- a/src/Pure/Isar/isar_output.ML Sat Dec 09 18:05:34 2006 +0100
+++ b/src/Pure/Isar/isar_output.ML Sat Dec 09 18:05:36 2006 +0100
@@ -441,6 +441,8 @@
val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.revert_skolems ctxt;
+fun pretty_term_abbrev ctxt =
+ ProofContext.pretty_term_abbrev ctxt o ProofContext.revert_skolems ctxt;
fun pretty_term_typ ctxt t =
ProofContext.pretty_term ctxt (TypeInfer.constrain t (Term.fastype_of t));
@@ -451,6 +453,16 @@
if Term.is_Const t then pretty_term ctxt t
else error ("Logical constant expected: " ^ ProofContext.string_of_term ctxt t);
+fun pretty_abbrev ctxt t =
+ let
+ fun err () = error ("Abbreviated constant expected: " ^ ProofContext.string_of_term ctxt t);
+ val (head, args) = Term.strip_comb t;
+ val (c, T) = Term.dest_Const head handle TERM _ => err ();
+ val (U, (u, _)) = Consts.the_abbreviation (ProofContext.consts_of ctxt) c
+ handle TYPE _ => err ();
+ val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
+ in pretty_term_abbrev ctxt (Logic.mk_equals (t, t')) end;
+
fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
fun pretty_term_style ctxt (name, t) =
@@ -517,6 +529,7 @@
("term_type", args Args.term (output pretty_term_typ)),
("typeof", args Args.term (output pretty_term_typeof)),
("const", args Args.term (output pretty_term_const)),
+ ("abbrev", args Args.term_abbrev (output pretty_abbrev)),
("typ", args Args.typ_abbrev (output ProofContext.pretty_typ)),
("text", args (Scan.lift Args.name) (output (K pretty_text))),
("goals", output_goals true),