src/Pure/Isar/proof.ML
changeset 12930 c1f3ff5feff1
parent 12808 a529b4b91888
child 12959 bf48fd86a732
equal deleted inserted replaced
12929:dbac8831d954 12930:c1f3ff5feff1
    57     (thm list * context attribute list) list) list -> state -> state
    57     (thm list * context attribute list) list) list -> state -> state
    58   val with_thmss: ((bstring * context attribute list) *
    58   val with_thmss: ((bstring * context attribute list) *
    59     (xstring * context attribute list) list) list -> state -> state
    59     (xstring * context attribute list) list) list -> state -> state
    60   val with_thmss_i: ((bstring * context attribute list) *
    60   val with_thmss_i: ((bstring * context attribute list) *
    61     (thm list * context attribute list) list) list -> state -> state
    61     (thm list * context attribute list) list) list -> state -> state
       
    62   val using_thmss: ((xstring * context attribute list) list) list -> state -> state
       
    63   val using_thmss_i: ((thm list * context attribute list) list) list -> state -> state
    62   val fix: (string list * string option) list -> state -> state
    64   val fix: (string list * string option) list -> state -> state
    63   val fix_i: (string list * typ option) list -> state -> state
    65   val fix_i: (string list * typ option) list -> state -> state
    64   val assm: ProofContext.exporter
    66   val assm: ProofContext.exporter
    65     -> ((string * context attribute list) * (string * (string list * string list)) list) list
    67     -> ((string * context attribute list) * (string * (string list * string list)) list) list
    66     -> state -> state
    68     -> state -> state
   541 val with_thmss_i = gen_with_thmss have_thmss_i;
   543 val with_thmss_i = gen_with_thmss have_thmss_i;
   542 
   544 
   543 end;
   545 end;
   544 
   546 
   545 
   547 
       
   548 (* using_thmss *)
       
   549 
       
   550 local
       
   551 
       
   552 fun gen_using_thmss f args state =
       
   553   state
       
   554   |> assert_backward
       
   555   |> map_context_result (f (map (pair ("", [])) args))
       
   556   |> (fn (st, named_facts) =>
       
   557     let val (_, (_, ((result, (facts, thm)), f))) = find_goal st;
       
   558     in st |> map_goal I (K ((result, (facts @ flat (map snd named_facts), thm)), f)) end);
       
   559 
       
   560 in
       
   561 
       
   562 val using_thmss = gen_using_thmss ProofContext.have_thmss;
       
   563 val using_thmss_i = gen_using_thmss ProofContext.have_thmss_i;
       
   564 
       
   565 end;
       
   566 
       
   567 
   546 (* fix *)
   568 (* fix *)
   547 
   569 
   548 fun gen_fix f xs state =
   570 fun gen_fix f xs state =
   549   state
   571   state
   550   |> assert_forward
   572   |> assert_forward