@{lemma}: allow terminal method;
authorwenzelm
Thu Jul 10 13:37:35 2008 +0200 (2008-07-10)
changeset 27522b819d3b263a0
parent 27521 44081396d735
child 27523 56eb04c7b6b2
@{lemma}: allow terminal method;
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Thy/thy_output.ML	Thu Jul 10 13:37:34 2008 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Jul 10 13:37:35 2008 +0200
     1.3 @@ -463,13 +463,6 @@
     1.4      val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
     1.5    in pretty_term_abbrev ctxt (Logic.mk_equals (t, t')) end;
     1.6  
     1.7 -fun pretty_lemma ctxt (prop, method_text) =
     1.8 -  let
     1.9 -    val _ = ctxt
    1.10 -      |> Proof.theorem_i NONE (K I) [[(prop, [])]]
    1.11 -      |> Proof.global_terminal_proof (method_text, NONE);
    1.12 -  in pretty_term ctxt prop end;
    1.13 -
    1.14  fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
    1.15  
    1.16  fun pretty_term_style ctxt (name, t) =
    1.17 @@ -525,12 +518,22 @@
    1.18      #> space_implode "\\isasep\\isanewline%\n"));
    1.19  
    1.20  
    1.21 -(* commands *)
    1.22 +(* embedded lemmas *)
    1.23 +
    1.24 +fun pretty_lemma ctxt (prop, methods) =
    1.25 +  let
    1.26 +    val _ = ctxt
    1.27 +      |> Proof.theorem_i NONE (K I) [[(prop, [])]]
    1.28 +      |> Proof.global_terminal_proof methods;
    1.29 +  in pretty_term ctxt prop end;
    1.30  
    1.31  val embedded_lemma =
    1.32 -  args (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse_args))
    1.33 +  args (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse_args -- Scan.option Method.parse_args))
    1.34      (output pretty_lemma o (fn ((a, arg :: _), p) => (Args.src ((a, [arg]), p))) o Args.dest_src);
    1.35  
    1.36 +
    1.37 +(* commands *)
    1.38 +
    1.39  val _ = OuterKeyword.keyword "by";
    1.40  
    1.41  val _ = add_commands