signature PSet_ind = sig type tactic = Abbrev.tactic val SET_INDUCT_TAC : Thm.thm -> tactic end
HOL 4, Kananaskis-14