# HG changeset patch
# User wenzelm
# Date 1165683936 -3600
# Node ID 410ca6910f6ff9b0b95237e5aa047fbf72b47df5
# Parent  8fcacb0e3b15d3fc3d22d2455e560fcf9068a47d
added antiquotation abbrev;

diff -r 8fcacb0e3b15 -r 410ca6910f6f NEWS
--- 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 ***
 
diff -r 8fcacb0e3b15 -r 410ca6910f6f doc-src/IsarRef/syntax.tex
--- 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$.
 
diff -r 8fcacb0e3b15 -r 410ca6910f6f src/Pure/Isar/isar_output.ML
--- 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),