added refine_insert;
authorwenzelm
Thu Feb 02 16:31:37 2006 +0100 (2006-02-02)
changeset 18908fb080097e436
parent 18907 f984f22f1cb4
child 18909 f1333b0ff9e5
added refine_insert;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Thu Feb 02 16:31:35 2006 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Thu Feb 02 16:31:37 2006 +0100
     1.3 @@ -36,6 +36,7 @@
     1.4    val pretty_goals: bool -> state -> Pretty.T list
     1.5    val refine: Method.text -> state -> state Seq.seq
     1.6    val refine_end: Method.text -> state -> state Seq.seq
     1.7 +  val refine_insert: thm list -> state -> state
     1.8    val refine_goals: (context -> thm -> unit) -> context -> thm list -> state -> state Seq.seq
     1.9    val match_bind: (string list * string) list -> state -> state
    1.10    val match_bind_i: (term list * term) list -> state -> state
    1.11 @@ -422,6 +423,9 @@
    1.12  val refine = apply_text true;
    1.13  val refine_end = apply_text false;
    1.14  
    1.15 +fun refine_insert [] = I
    1.16 +  | refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths)));
    1.17 +
    1.18  end;
    1.19  
    1.20