src/Pure/Isar/proof.ML
changeset 38333 3f4fadad9497
parent 38218 1408f753bd75
child 38721 ca8b14fa0d0d
equal deleted inserted replaced
38332:6551e310e7cb 38333:3f4fadad9497
    58   val presume_cmd: (Attrib.binding * (string * string list) list) list -> state -> state
    58   val presume_cmd: (Attrib.binding * (string * string list) list) list -> state -> state
    59   val def: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state
    59   val def: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state
    60   val def_cmd: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
    60   val def_cmd: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
    61   val chain: state -> state
    61   val chain: state -> state
    62   val chain_facts: thm list -> state -> state
    62   val chain_facts: thm list -> state -> state
    63   val get_thmss_cmd: state -> (Facts.ref * Attrib.src list) list -> thm list
       
    64   val note_thmss: (Thm.binding * (thm list * attribute list) list) list -> state -> state
    63   val note_thmss: (Thm.binding * (thm list * attribute list) list) list -> state -> state
    65   val note_thmss_cmd: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
    64   val note_thmss_cmd: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
    66   val from_thmss: ((thm list * attribute list) list) list -> state -> state
    65   val from_thmss: ((thm list * attribute list) list) list -> state -> state
    67   val from_thmss_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
    66   val from_thmss_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
    68   val with_thmss: ((thm list * attribute list) list) list -> state -> state
    67   val with_thmss: ((thm list * attribute list) list) list -> state -> state
   677 val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
   676 val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
   678 val with_thmss_cmd = gen_thmss the_facts chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
   677 val with_thmss_cmd = gen_thmss the_facts chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
   679 
   678 
   680 val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
   679 val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
   681 
   680 
   682 fun get_thmss_cmd state srcs = the_facts (note_thmss_cmd [((Binding.empty, []), srcs)] state);
       
   683 
       
   684 end;
   681 end;
   685 
   682 
   686 
   683 
   687 (* using/unfolding *)
   684 (* using/unfolding *)
   688 
   685