src/Pure/Isar/proof_context.ML
changeset 6875 df31250ccb3a
parent 6870 43d64c520d11
child 6895 450b1f67f099
equal deleted inserted replaced
6874:747f656e04ec 6875:df31250ccb3a
    42   val get_thms: context -> string -> thm list
    42   val get_thms: context -> string -> thm list
    43   val get_thmss: context -> string list -> thm list
    43   val get_thmss: context -> string list -> thm list
    44   val put_thm: string * thm -> context -> context
    44   val put_thm: string * thm -> context -> context
    45   val put_thms: string * thm list -> context -> context
    45   val put_thms: string * thm list -> context -> context
    46   val put_thmss: (string * thm list) list -> context -> context
    46   val put_thmss: (string * thm list) list -> context -> context
    47   val have_thmss: string -> context attribute list
    47   val have_thmss: thm list -> string -> context attribute list
    48     -> (thm list * context attribute list) list -> context -> context * (string * thm list)
    48     -> (thm list * context attribute list) list -> context -> context * (string * thm list)
    49   val assumptions: context -> (cterm * (int -> tactic)) list
    49   val assumptions: context -> (cterm * (int -> tactic)) list
    50   val fixed_names: context -> string list
    50   val fixed_names: context -> string list
    51   val assume: (int -> tactic) -> string -> context attribute list -> (string * string list) list
    51   val assume: (int -> tactic) -> string -> context attribute list -> (string * string list) list
    52     -> context -> context * ((string * thm list) * thm list)
    52     -> context -> context * ((string * thm list) * thm list)
   615   | put_thmss (th :: ths) ctxt = ctxt |> put_thms th |> put_thmss ths;
   615   | put_thmss (th :: ths) ctxt = ctxt |> put_thms th |> put_thmss ths;
   616 
   616 
   617 
   617 
   618 (* have_thmss *)
   618 (* have_thmss *)
   619 
   619 
   620 fun have_thmss name more_attrs ths_attrs ctxt =
   620 fun have_thmss more_ths name more_attrs ths_attrs ctxt =
   621   let
   621   let
   622     fun app ((ct, ths), (th, attrs)) =
   622     fun app ((ct, ths), (th, attrs)) =
   623       let val (ct', th') = Thm.applys_attributes ((ct, th), attrs @ more_attrs)
   623       let val (ct', th') = Thm.applys_attributes ((ct, th), attrs @ more_attrs)
   624       in (ct', th' :: ths) end
   624       in (ct', th' :: ths) end
   625     val (ctxt', rev_thms) = foldl app ((ctxt, []), ths_attrs);
   625     val (ctxt', rev_thms) = foldl app ((ctxt, []), ths_attrs);
   626     val thms = flat (rev rev_thms);
   626     val thms = flat (rev rev_thms) @ more_ths;
   627   in (ctxt' |> put_thms (name, thms), (name, thms)) end;
   627   in (ctxt' |> put_thms (name, thms), (name, thms)) end;
   628 
   628 
   629 
   629 
   630 
   630 
   631 (** assumptions **)
   631 (** assumptions **)
   652 
   652 
   653     val ths = map (fn th => ([th], [])) asms;
   653     val ths = map (fn th => ([th], [])) asms;
   654     val (ctxt'', (_, thms)) =
   654     val (ctxt'', (_, thms)) =
   655       ctxt'
   655       ctxt'
   656       |> auto_bind_facts name props
   656       |> auto_bind_facts name props
   657       |> have_thmss name (attrs @ [Drule.tag_assumption]) ths;
   657       |> have_thmss [] name (attrs @ [Drule.tag_assumption]) ths;
   658 
   658 
   659     val ctxt''' =
   659     val ctxt''' =
   660       ctxt''
   660       ctxt''
   661       |> map_context (fn (thy, data, ((asms_ct, asms_th), fixes), binds, thms, defs) =>
   661       |> map_context (fn (thy, data, ((asms_ct, asms_th), fixes), binds, thms, defs) =>
   662         (thy, data, ((asms_ct @ cprops_tac, asms_th @ [(name, asms)]), fixes), binds, thms, defs));
   662         (thy, data, ((asms_ct @ cprops_tac, asms_th @ [(name, asms)]), fixes), binds, thms, defs));