@{lemma}: 'by' keyword;

--- a/NEWS	Sat Jun 28 15:30:46 2008 +0200
+++ b/NEWS	Sat Jun 28 21:21:13 2008 +0200
@@ -19,6 +19,12 @@
 interface instead.
 
 
+*** Document preparation ***
+
+* Antiquotation @{lemma} now imitates a regular terminal proof,
+demanding keyword 'by' and supporting the full method expressions.
+
+
 *** HOL ***
 
 * Methods "case_tac" and "induct_tac" now refer to the very same rules

--- a/src/HOL/List.thy	Sat Jun 28 15:30:46 2008 +0200
+++ b/src/HOL/List.thy	Sat Jun 28 21:21:13 2008 +0200
@@ -215,40 +215,40 @@
 \begin{figure}[htbp]
 \fbox{
 \begin{tabular}{l}
-@{lemma "[a,b]@[c,d] = [a,b,c,d]" simp}\\
-@{lemma "length [a,b,c] = 3" simp}\\
-@{lemma "set [a,b,c] = {a,b,c}" simp}\\
-@{lemma "map f [a,b,c] = [f a, f b, f c]" simp}\\
-@{lemma "rev [a,b,c] = [c,b,a]" simp}\\
-@{lemma "hd [a,b,c,d] = a" simp}\\
-@{lemma "tl [a,b,c,d] = [b,c,d]" simp}\\
-@{lemma "last [a,b,c,d] = d" simp}\\
-@{lemma "butlast [a,b,c,d] = [a,b,c]" simp}\\
-@{lemma[source] "filter (\<lambda>n::nat. n<2) [0,2,1] = [0,1]" simp}\\
-@{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" simp}\\
-@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" simp}\\
-@{lemma "foldr f [a,b,c] x = f a (f b (f c x))" simp}\\
-@{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" simp}\\
-@{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" simp}\\
-@{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" simp}\\
-@{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" simp}\\
-@{lemma "take 2 [a,b,c,d] = [a,b]" simp}\\
-@{lemma "take 6 [a,b,c,d] = [a,b,c,d]" simp}\\
-@{lemma "drop 2 [a,b,c,d] = [c,d]" simp}\\
-@{lemma "drop 6 [a,b,c,d] = []" simp}\\
-@{lemma "takeWhile (%n::nat. n<3) [1,2,3,0] = [1,2]" simp}\\
-@{lemma "dropWhile (%n::nat. n<3) [1,2,3,0] = [3,0]" simp}\\
-@{lemma "distinct [2,0,1::nat]" simp}\\
-@{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" simp}\\
-@{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" simp}\\
-@{lemma "nth [a,b,c,d] 2 = c" simp}\\
-@{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" simp}\\
-@{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" (simp add:sublist_def)}\\
-@{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" (simp add:rotate1_def)}\\
-@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" (simp add:rotate1_def rotate_def nat_number)}\\
-@{lemma "replicate 4 a = [a,a,a,a]" (simp add:nat_number)}\\
-@{lemma "[2..<5] = [2,3,4]" (simp add:nat_number)}\\
-@{lemma "listsum [1,2,3::nat] = 6" simp}
+@{lemma "[a,b]@[c,d] = [a,b,c,d]" by simp}\\
+@{lemma "length [a,b,c] = 3" by simp}\\
+@{lemma "set [a,b,c] = {a,b,c}" by simp}\\
+@{lemma "map f [a,b,c] = [f a, f b, f c]" by simp}\\
+@{lemma "rev [a,b,c] = [c,b,a]" by simp}\\
+@{lemma "hd [a,b,c,d] = a" by simp}\\
+@{lemma "tl [a,b,c,d] = [b,c,d]" by simp}\\
+@{lemma "last [a,b,c,d] = d" by simp}\\
+@{lemma "butlast [a,b,c,d] = [a,b,c]" by simp}\\
+@{lemma[source] "filter (\<lambda>n::nat. n<2) [0,2,1] = [0,1]" by simp}\\
+@{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" by simp}\\
+@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\
+@{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by simp}\\
+@{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\
+@{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\
+@{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
+@{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\
+@{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\
+@{lemma "take 6 [a,b,c,d] = [a,b,c,d]" by simp}\\
+@{lemma "drop 2 [a,b,c,d] = [c,d]" by simp}\\
+@{lemma "drop 6 [a,b,c,d] = []" by simp}\\
+@{lemma "takeWhile (%n::nat. n<3) [1,2,3,0] = [1,2]" by simp}\\
+@{lemma "dropWhile (%n::nat. n<3) [1,2,3,0] = [3,0]" by simp}\\
+@{lemma "distinct [2,0,1::nat]" by simp}\\
+@{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\
+@{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\
+@{lemma "nth [a,b,c,d] 2 = c" by simp}\\
+@{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
+@{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
+@{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by (simp add:rotate1_def)}\\
+@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def nat_number)}\\
+@{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number)}\\
+@{lemma "[2..<5] = [2,3,4]" by (simp add:nat_number)}\\
+@{lemma "listsum [1,2,3::nat] = 6" by simp}
 \end{tabular}}
 \caption{Characteristic examples}
 \label{fig:Characteristic}

--- a/src/Pure/Thy/thy_output.ML	Sat Jun 28 15:30:46 2008 +0200
+++ b/src/Pure/Thy/thy_output.ML	Sat Jun 28 21:21:13 2008 +0200
@@ -463,15 +463,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) =
+fun pretty_lemma 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;
 
-val hd_src = Args.src o (apfst o apsnd) (single o hd) o Args.dest_src;
-
 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
 
 fun pretty_term_style ctxt (name, t) =
@@ -529,11 +527,17 @@
 
 (* commands *)
 
+val embedded_lemma =
+  args (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse_args))
+    (output pretty_lemma o (fn ((a, arg :: _), p) => (Args.src ((a, [arg]), p))) o Args.dest_src);
+
+val _ = OuterKeyword.keyword "by";
+
 val _ = add_commands
  [("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 o hd_src)),
+  ("lemma", embedded_lemma),
   ("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)),