1signature mp_then =
2sig
3
4  include Abbrev
5
6  datatype match_position = datatype thmpos_dtype.match_position
7  val mp_then : match_position -> thm_tactic -> thm -> thm -> tactic
8
9end
10