# HG changeset patch
# User haftmann
# Date 1209491702 -7200
# Node ID 78ed28528ca670174d8fd2471075ec3c9baa80cd
# Parent  190da765a628512789d097c866bf4aa2f73f5725
added lemma antiquotation

diff -r 190da765a628 -r 78ed28528ca6 NEWS
--- a/NEWS	Tue Apr 29 15:25:50 2008 +0200
+++ b/NEWS	Tue Apr 29 19:55:02 2008 +0200
@@ -98,6 +98,16 @@
 situations.
 
 
+*** Document preparation ***
+
+* Antiquotation "lemma" takes a proposition and a simple method text as argument
+and asserts that the proposition is provable by the corresponding method
+invocation.  Prints text of proposition, as does antiquotation "prop".  A simple
+method text is either a method name or a method name plus (optional) method
+arguments in parentheses, mimicing the conventions known from Isar proof text.
+Useful for illustration of presented theorems by particular examples.
+
+
 *** HOL ***
 
 * Merged theories Wellfounded_Recursion, Accessible_Part and Wellfounded_Relations
diff -r 190da765a628 -r 78ed28528ca6 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Apr 29 15:25:50 2008 +0200
+++ b/src/Pure/Isar/method.ML	Tue Apr 29 19:55:02 2008 +0200
@@ -79,6 +79,7 @@
   val method_setup: bstring -> string * Position.T -> string -> theory -> theory
   val syntax: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list))
     -> src -> Proof.context -> 'a * Proof.context
+  val simple_text: Args.T list -> text * Args.T list
   val simple_args: (Args.T list -> 'a * Args.T list)
     -> ('a -> Proof.context -> method) -> src -> Proof.context -> method
   val ctxt_args: (Proof.context -> method) -> src -> Proof.context -> method
@@ -467,6 +468,11 @@
 
 fun syntax scan = Args.context_syntax "method" scan;
 
+val simple_text = (Args.$$$ "(" |-- Args.name
+    -- Scan.repeat (Scan.one (fn x => not (Args.string_of x = ")"))) --| Args.$$$ ")"
+  || Args.name -- Scan.succeed [])
+  >> (fn (name, args) => Source (Args.src ((name, args), Position.none)));
+
 fun simple_args scan f src ctxt : method =
   fst (syntax (Scan.lift (scan >> (fn x => f x ctxt))) src ctxt);
 
diff -r 190da765a628 -r 78ed28528ca6 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Apr 29 15:25:50 2008 +0200
+++ b/src/Pure/Thy/thy_output.ML	Tue Apr 29 19:55:02 2008 +0200
@@ -456,6 +456,13 @@
     val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
   in pretty_term_abbrev ctxt (Logic.mk_equals (t, t')) end;
 
+fun pretty_fact ctxt (prop, method_text) =
+  let
+    val _ = ctxt
+      |> Proof.theorem_i NONE (K I) [[(prop, [])]]
+      |> Proof.global_terminal_proof (method_text, NONE);
+  in pretty_term ctxt prop end;
+
 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
 
 fun pretty_term_style ctxt (name, t) =
@@ -517,6 +524,7 @@
  [("thm", args Attrib.thms (output_list pretty_thm)),
   ("thm_style", args (Scan.lift Args.liberal_name -- Attrib.thm) (output pretty_thm_style)),
   ("prop", args Args.prop (output pretty_term)),
+  ("lemma", args (Args.prop -- Scan.lift Method.simple_text) (output pretty_fact)),
   ("term", args Args.term (output pretty_term)),
   ("term_style", args (Scan.lift Args.liberal_name -- Args.term) (output pretty_term_style)),
   ("term_type", args Args.term (output pretty_term_typ)),