1signature oneSyntax =
2sig
3  include Abbrev
4
5  val one_ty      : hol_type
6  val one_tm      : term
7  val one_case_tm : term
8  val mk_one_case : term -> term
9  val lift_one    : hol_type -> unit -> term
10  val is_one      : term -> bool
11end
12