Lines Matching defs:thms
66 fun datatype_thms thms =
67 thms @ [cond_rand_thms, snd_exception_thms, FST_SWAP,
122 fun addThms thms = (rwts := thms @ !rwts; thms)
589 val thms = ref ([dim_thm, wordsTheory.bit_count_def] @ wbit_thms) *)
590 val thms = ref wbit_thms
591 val c = ref (PURE_REWRITE_CONV (!thms))
627 val () = thms := !thms @ (bit_count_thms v)
628 val () = c := PURE_REWRITE_CONV (!thms)