1.1 --- a/NEWS	Sat Jun 28 15:30:46 2008 +0200
     1.2 +++ b/NEWS	Sat Jun 28 21:21:13 2008 +0200
     1.3 @@ -19,6 +19,12 @@
     1.4  interface instead.
     1.5  
     1.6  
     1.7 +*** Document preparation ***
     1.8 +
     1.9 +* Antiquotation @{lemma} now imitates a regular terminal proof,
    1.10 +demanding keyword 'by' and supporting the full method expressions.
    1.11 +
    1.12 +
    1.13  *** HOL ***
    1.14  
    1.15  * Methods "case_tac" and "induct_tac" now refer to the very same rules

     2.1 --- a/src/HOL/List.thy	Sat Jun 28 15:30:46 2008 +0200
     2.2 +++ b/src/HOL/List.thy	Sat Jun 28 21:21:13 2008 +0200
     2.3 @@ -215,40 +215,40 @@
     2.4  \begin{figure}[htbp]
     2.5  \fbox{
     2.6  \begin{tabular}{l}
     2.7 -@{lemma "[a,b]@[c,d] = [a,b,c,d]" simp}\\
     2.8 -@{lemma "length [a,b,c] = 3" simp}\\
     2.9 -@{lemma "set [a,b,c] = {a,b,c}" simp}\\
    2.10 -@{lemma "map f [a,b,c] = [f a, f b, f c]" simp}\\
    2.11 -@{lemma "rev [a,b,c] = [c,b,a]" simp}\\
    2.12 -@{lemma "hd [a,b,c,d] = a" simp}\\
    2.13 -@{lemma "tl [a,b,c,d] = [b,c,d]" simp}\\
    2.14 -@{lemma "last [a,b,c,d] = d" simp}\\
    2.15 -@{lemma "butlast [a,b,c,d] = [a,b,c]" simp}\\
    2.16 -@{lemma[source] "filter (\<lambda>n::nat. n<2) [0,2,1] = [0,1]" simp}\\
    2.17 -@{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" simp}\\
    2.18 -@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" simp}\\
    2.19 -@{lemma "foldr f [a,b,c] x = f a (f b (f c x))" simp}\\
    2.20 -@{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" simp}\\
    2.21 -@{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" simp}\\
    2.22 -@{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" simp}\\
    2.23 -@{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" simp}\\
    2.24 -@{lemma "take 2 [a,b,c,d] = [a,b]" simp}\\
    2.25 -@{lemma "take 6 [a,b,c,d] = [a,b,c,d]" simp}\\
    2.26 -@{lemma "drop 2 [a,b,c,d] = [c,d]" simp}\\
    2.27 -@{lemma "drop 6 [a,b,c,d] = []" simp}\\
    2.28 -@{lemma "takeWhile (%n::nat. n<3) [1,2,3,0] = [1,2]" simp}\\
    2.29 -@{lemma "dropWhile (%n::nat. n<3) [1,2,3,0] = [3,0]" simp}\\
    2.30 -@{lemma "distinct [2,0,1::nat]" simp}\\
    2.31 -@{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" simp}\\
    2.32 -@{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" simp}\\
    2.33 -@{lemma "nth [a,b,c,d] 2 = c" simp}\\
    2.34 -@{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" simp}\\
    2.35 -@{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" (simp add:sublist_def)}\\
    2.36 -@{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" (simp add:rotate1_def)}\\
    2.37 -@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" (simp add:rotate1_def rotate_def nat_number)}\\
    2.38 -@{lemma "replicate 4 a = [a,a,a,a]" (simp add:nat_number)}\\
    2.39 -@{lemma "[2..<5] = [2,3,4]" (simp add:nat_number)}\\
    2.40 -@{lemma "listsum [1,2,3::nat] = 6" simp}
    2.41 +@{lemma "[a,b]@[c,d] = [a,b,c,d]" by simp}\\
    2.42 +@{lemma "length [a,b,c] = 3" by simp}\\
    2.43 +@{lemma "set [a,b,c] = {a,b,c}" by simp}\\
    2.44 +@{lemma "map f [a,b,c] = [f a, f b, f c]" by simp}\\
    2.45 +@{lemma "rev [a,b,c] = [c,b,a]" by simp}\\
    2.46 +@{lemma "hd [a,b,c,d] = a" by simp}\\
    2.47 +@{lemma "tl [a,b,c,d] = [b,c,d]" by simp}\\
    2.48 +@{lemma "last [a,b,c,d] = d" by simp}\\
    2.49 +@{lemma "butlast [a,b,c,d] = [a,b,c]" by simp}\\
    2.50 +@{lemma[source] "filter (\<lambda>n::nat. n<2) [0,2,1] = [0,1]" by simp}\\
    2.51 +@{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" by simp}\\
    2.52 +@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\
    2.53 +@{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by simp}\\
    2.54 +@{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\
    2.55 +@{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\
    2.56 +@{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
    2.57 +@{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\
    2.58 +@{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\
    2.59 +@{lemma "take 6 [a,b,c,d] = [a,b,c,d]" by simp}\\
    2.60 +@{lemma "drop 2 [a,b,c,d] = [c,d]" by simp}\\
    2.61 +@{lemma "drop 6 [a,b,c,d] = []" by simp}\\
    2.62 +@{lemma "takeWhile (%n::nat. n<3) [1,2,3,0] = [1,2]" by simp}\\
    2.63 +@{lemma "dropWhile (%n::nat. n<3) [1,2,3,0] = [3,0]" by simp}\\
    2.64 +@{lemma "distinct [2,0,1::nat]" by simp}\\
    2.65 +@{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\
    2.66 +@{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\
    2.67 +@{lemma "nth [a,b,c,d] 2 = c" by simp}\\
    2.68 +@{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
    2.69 +@{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
    2.70 +@{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by (simp add:rotate1_def)}\\
    2.71 +@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def nat_number)}\\
    2.72 +@{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number)}\\
    2.73 +@{lemma "[2..<5] = [2,3,4]" by (simp add:nat_number)}\\
    2.74 +@{lemma "listsum [1,2,3::nat] = 6" by simp}
    2.75  \end{tabular}}
    2.76  \caption{Characteristic examples}
    2.77  \label{fig:Characteristic}

     3.1 --- a/src/Pure/Thy/thy_output.ML	Sat Jun 28 15:30:46 2008 +0200
     3.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Jun 28 21:21:13 2008 +0200
     3.3 @@ -463,15 +463,13 @@
     3.4      val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
     3.5    in pretty_term_abbrev ctxt (Logic.mk_equals (t, t')) end;
     3.6  
     3.7 -fun pretty_fact ctxt (prop, method_text) =
     3.8 +fun pretty_lemma ctxt (prop, method_text) =
     3.9    let
    3.10      val _ = ctxt
    3.11        |> Proof.theorem_i NONE (K I) [[(prop, [])]]
    3.12        |> Proof.global_terminal_proof (method_text, NONE);
    3.13    in pretty_term ctxt prop end;
    3.14  
    3.15 -val hd_src = Args.src o (apfst o apsnd) (single o hd) o Args.dest_src;
    3.16 -
    3.17  fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
    3.18  
    3.19  fun pretty_term_style ctxt (name, t) =
    3.20 @@ -529,11 +527,17 @@
    3.21  
    3.22  (* commands *)
    3.23  
    3.24 +val embedded_lemma =
    3.25 +  args (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse_args))
    3.26 +    (output pretty_lemma o (fn ((a, arg :: _), p) => (Args.src ((a, [arg]), p))) o Args.dest_src);
    3.27 +
    3.28 +val _ = OuterKeyword.keyword "by";
    3.29 +
    3.30  val _ = add_commands
    3.31   [("thm", args Attrib.thms (output_list pretty_thm)),
    3.32    ("thm_style", args (Scan.lift Args.liberal_name -- Attrib.thm) (output pretty_thm_style)),
    3.33    ("prop", args Args.prop (output pretty_term)),
    3.34 -  ("lemma", args (Args.prop -- Scan.lift Method.simple_text) (output pretty_fact o hd_src)),
    3.35 +  ("lemma", embedded_lemma),
    3.36    ("term", args Args.term (output pretty_term)),
    3.37    ("term_style", args (Scan.lift Args.liberal_name -- Args.term) (output pretty_term_style)),
    3.38    ("term_type", args Args.term (output pretty_term_typ)),