Lines Matching defs:thms
355 val thms = Drule.CONJUNCTS (Q.SPEC `t` boolTheory.IMP_CLAUSES)
356 val T_imp = Drule.GEN_ALL (hd thms)
357 val F_imp = Drule.GEN_ALL (List.nth (thms, 2))
467 fun SRW_CONV thms = SIMP_CONV (srw_ss()) thms
470 fun SRW_RULE thms = Conv.CONV_RULE (SRW_CONV thms)
790 val thms =
795 find_rw (mk_rw_net lhsc thms)
878 fun specialized msg ctms thms =
881 val () = print ("Specializing " ^ msg ^ ": " ^ sz thms ^ " -> ")
883 val r = List.mapPartial (specialize ctms) thms
1068 fun theory_rewrites (thms, i: inventory) =
1070 val thm_names = List.map get_name thms
1074 List.map (fn t => DB.fetch thy t) (l @ m) @ thms