src/Provers/blast.ML
changeset 30513 1796b8ea88aa
parent 30320 5f859035331f
child 30541 9f168bdc468a
equal deleted inserted replaced
30512:17b2aad869fa 30513:1796b8ea88aa
    54                  hazIs: thm list, hazEs: thm list,
    54                  hazIs: thm list, hazEs: thm list,
    55                  swrappers: (string * wrapper) list,
    55                  swrappers: (string * wrapper) list,
    56                  uwrappers: (string * wrapper) list,
    56                  uwrappers: (string * wrapper) list,
    57                  safe0_netpair: netpair, safep_netpair: netpair,
    57                  safe0_netpair: netpair, safep_netpair: netpair,
    58                  haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: ContextRules.netpair}
    58                  haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: ContextRules.netpair}
    59   val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    59   val cla_modifiers: Method.modifier parser list
    60   val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
    60   val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
    61   end;
    61   end;
    62 
    62 
    63 
    63 
    64 signature BLAST =
    64 signature BLAST =