Lines Matching defs:thms
77 abstype rewrites = RW of {thms : thm list, net : conv Net.net}
79 fun dest_rewrites(RW{thms, ...}) = thms
81 val empty_rewrites = RW{thms = [], net= Net.empty}
86 fun add_rewrites (RW{thms,net}) thl =
91 RW{thms = thms@thl,
258 val thms = dest_rewrites rws
259 val thms' = flatten (map mk_rewrites thms)
260 val how_many = length thms'
266 pr_list pp_thm (add_string";" >> add_break(2,0)) thms'