1signature Witness = 2sig 3 include Abbrev 4 5 val find_inductive_witnesses 6 : thm list -> thm option list -> thm list -> thm list 7 8end 9