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