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