Structure mp_then

Source File	Identifier index	Theory binding index

signature mp_then =
sig

  include Abbrev

  datatype match_position = datatype thmpos_dtype.match_position
  val mp_then : match_position -> thm_tactic -> thm -> thm -> tactic

end

Source File	Identifier index	Theory binding index

HOL 4, Kananaskis-14