src/Pure/Isar/proof.ML
changeset 6876 4ae9c47f2b6b
parent 6871 01866edde713
child 6887 12b5fb35a688
     1.1 --- a/src/Pure/Isar/proof.ML	Thu Jul 01 21:20:27 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Thu Jul 01 21:20:57 1999 +0200
     1.3 @@ -31,8 +31,9 @@
     1.4    val bind_i: (indexname * term) list -> state -> state
     1.5    val match_bind: (string list * string) list -> state -> state
     1.6    val match_bind_i: (term list * term) list -> state -> state
     1.7 -  val have_thmss: string -> context attribute list ->
     1.8 +  val have_thmss: thm list -> string -> context attribute list ->
     1.9      (thm list * context attribute list) list -> state -> state
    1.10 +  val simple_have_thms: string -> thm list -> state -> state
    1.11    val assume: (int -> tactic) -> string -> context attribute list -> (string * string list) list
    1.12      -> state -> state
    1.13    val assume_i: (int -> tactic) -> string -> context attribute list -> (term * term list) list
    1.14 @@ -436,12 +437,14 @@
    1.15  
    1.16  (* have_thmss *)
    1.17  
    1.18 -fun have_thmss name atts ths_atts state =
    1.19 +fun have_thmss ths name atts ths_atts state =
    1.20    state
    1.21    |> assert_forward
    1.22 -  |> map_context_result (ProofContext.have_thmss (PureThy.default_name name) atts ths_atts)
    1.23 +  |> map_context_result (ProofContext.have_thmss ths (PureThy.default_name name) atts ths_atts)
    1.24    |> these_facts;
    1.25  
    1.26 +fun simple_have_thms name thms = have_thmss [] name [] [(thms, [])];
    1.27 +
    1.28  
    1.29  (* fix *)
    1.30  
    1.31 @@ -619,7 +622,7 @@
    1.32      state
    1.33      |> close_block
    1.34      |> auto_bind_facts name [t]
    1.35 -    |> have_thmss name atts [Thm.no_attributes [result]]
    1.36 +    |> have_thmss [] name atts [Thm.no_attributes [result]]
    1.37      |> opt_solve
    1.38    end;
    1.39