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