src/Pure/Isar/proof.ML
changeset 6876 4ae9c47f2b6b
parent 6871 01866edde713
child 6887 12b5fb35a688
equal deleted inserted replaced
6875:df31250ccb3a 6876:4ae9c47f2b6b
    29   val refine: (context -> method) -> state -> state Seq.seq
    29   val refine: (context -> method) -> state -> state Seq.seq
    30   val bind: (indexname * string) list -> state -> state
    30   val bind: (indexname * string) list -> state -> state
    31   val bind_i: (indexname * term) list -> state -> state
    31   val bind_i: (indexname * term) list -> state -> state
    32   val match_bind: (string list * string) list -> state -> state
    32   val match_bind: (string list * string) list -> state -> state
    33   val match_bind_i: (term list * term) list -> state -> state
    33   val match_bind_i: (term list * term) list -> state -> state
    34   val have_thmss: string -> context attribute list ->
    34   val have_thmss: thm list -> string -> context attribute list ->
    35     (thm list * context attribute list) list -> state -> state
    35     (thm list * context attribute list) list -> state -> state
       
    36   val simple_have_thms: string -> thm list -> state -> state
    36   val assume: (int -> tactic) -> string -> context attribute list -> (string * string list) list
    37   val assume: (int -> tactic) -> string -> context attribute list -> (string * string list) list
    37     -> state -> state
    38     -> state -> state
    38   val assume_i: (int -> tactic) -> string -> context attribute list -> (term * term list) list
    39   val assume_i: (int -> tactic) -> string -> context attribute list -> (term * term list) list
    39     -> state -> state
    40     -> state -> state
    40   val fix: (string * string option) list -> state -> state
    41   val fix: (string * string option) list -> state -> state
   434 val match_bind_i = gen_bind ProofContext.match_binds_i;
   435 val match_bind_i = gen_bind ProofContext.match_binds_i;
   435 
   436 
   436 
   437 
   437 (* have_thmss *)
   438 (* have_thmss *)
   438 
   439 
   439 fun have_thmss name atts ths_atts state =
   440 fun have_thmss ths name atts ths_atts state =
   440   state
   441   state
   441   |> assert_forward
   442   |> assert_forward
   442   |> map_context_result (ProofContext.have_thmss (PureThy.default_name name) atts ths_atts)
   443   |> map_context_result (ProofContext.have_thmss ths (PureThy.default_name name) atts ths_atts)
   443   |> these_facts;
   444   |> these_facts;
       
   445 
       
   446 fun simple_have_thms name thms = have_thmss [] name [] [(thms, [])];
   444 
   447 
   445 
   448 
   446 (* fix *)
   449 (* fix *)
   447 
   450 
   448 fun gen_fix f xs state =
   451 fun gen_fix f xs state =
   617   in
   620   in
   618     print_result {kind = kind_name kind, name = name, thm = result};
   621     print_result {kind = kind_name kind, name = name, thm = result};
   619     state
   622     state
   620     |> close_block
   623     |> close_block
   621     |> auto_bind_facts name [t]
   624     |> auto_bind_facts name [t]
   622     |> have_thmss name atts [Thm.no_attributes [result]]
   625     |> have_thmss [] name atts [Thm.no_attributes [result]]
   623     |> opt_solve
   626     |> opt_solve
   624   end;
   627   end;
   625 
   628 
   626 fun local_qed finalize print_result state =
   629 fun local_qed finalize print_result state =
   627   state
   630   state