1signature patricia_castsLib = 2sig 3 4 include Abbrev 5 6 type term_ptree = patriciaLib.term_ptree 7 type num = Arbnum.num 8 9 val dest_word_ptree : term -> num * term_ptree 10 val mk_word_ptree : num * term_ptree -> term 11 12 val add_cast_ptree_compset : computeLib.compset -> unit 13 val cast_ptree_compset : unit -> computeLib.compset 14 val CAST_PTREE_CONV : conv 15 16 val Define_mk_word_ptree : string * string -> num -> term_ptree -> thm * thm 17 val iDefine_mk_word_ptree : string * string -> int -> term_ptree -> thm * thm 18 19end 20