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