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