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