Lines Matching defs:thms
76 fun mips_thms thms =
77 thms @
104 val thms = ref ([]: thm list)
106 fun resetThms () = thms := []
108 utilsLib.specialized "" (utilsLib.WGROUND_CONV, tms) (!thms)
109 fun addThms ts = (thms := ts @ !thms; ts)
113 fun evr (rule:rule) thms c cvr = List.map rule o ev thms c cvr
115 fun EVR rule thms c cvr = addThms o evr rule thms c cvr
381 (* Load/Store thms and tools *)
450 fun merge_cases thms =
452 fun thm i = List.nth (thms, i)
464 fun merge_cases thms =
466 fun thm i = List.nth (thms, i)
483 fun store_rule thms =
485 (SIMP_CONV std_ss (Aligned_thms :: cond_rand_thms :: mem_thms @ thms))
1163 val thms = List.map (fn f => STATE_CONV (f tm))
1167 val thm = Drule.LIST_CONJ ([thm1, thm2, thm3] @ thms)