Lines Matching defs:lt
46 val lt = boolSyntax.list_mk_forall (fvl,tm)
47 val _ = (lthms := Splaymap.insert(!lthms,lt,LazyThm(fv,fvl,jf)))
48 val res = (SPECL fvl (ASSUME lt))
110 fun testlz s (jf:unit->Thm.thm) lt =
112 then let val th = prove_lthm lt (* just calling jf may fail if jf uses tactics and lt has lazy lemmas *)
113 handle ex => (dbgTools.CBTH (s^"_lz") lt;dbgTools.DTH (s^"_lz") lt;
115 in if (Term.compare(concl th,concl lt)=EQUAL)
117 else (dbgTools.CBTH s th; dbgTools.CBTH (s^"_lz") lt;dbgTools.DTH s th;dbgTools.DTH (s^"_lz") lt;