1structure oneSyntax :> oneSyntax =
2struct
3
4local open oneTheory in end;
5
6open HolKernel Abbrev;
7
8val one_ty = mk_thy_type{Tyop="one", Thy="one", Args=[]}
9
10val one_tm      = prim_mk_const{Thy="one",Name="one"}
11val one_case_tm = prim_mk_const{Thy="one",Name="one_CASE"}
12
13fun mk_one_case x =
14   list_mk_comb(inst[alpha |-> type_of x]one_case_tm,[one_tm,x])
15
16fun lift_one ty () = one_tm
17
18val is_one = aconv one_tm
19
20end
21