1signature Thm =
2sig
3
4  include FinalThm where type tag = Tag.tag
5                     and type hol_type = Type.hol_type
6                     and type term = Term.term
7end
8