Lines Matching defs:ant
59 let val (vs,(ant,conseq)) = (I ## dest_imp) (strip_forall tm)
62 val simpl = prove_asm monoset ant (#1 (dest_imp (concl srul)))
64 val newasm = list_mk_forall(vs,mk_imp(ant,list_mk_forall(cvs,conj2)))
66 in DISCH newasm (GENL vs (DISCH ant (GENL cvs thm2)))
69 (* rul is of form |- !vs. ant ==> conseq
70 with ant a conjunction of conditions and conseq of form
72 tm is of similar form but where ant has a const applied to args
84 let val (vs,(ant,conseq)) = (I ## dest_imp) (strip_forall tm)
88 (QCONV (DEPTH_CONV BETA_CONV) ant))
94 val thm2 = DISCH asm (GENL vs (DISCH ant (EQ_MP (SYM bth) thm1)))
314 then let val (ant,_) = dest_imp bdy
315 val hyps = strip_conj(snd(strip_exists ant))
318 let val (vs,(ant,conseq)) = (I##dest_imp) (strip_forall tm)
321 val (evs,hyp) = strip_exists ant
345 let val (ant,conseq) = dest_imp stm
346 val hthm = APPLY_CASE rfns ant
374 let val (vs,(ant,conseq)) = (I ## dest_imp) (strip_forall (concl th))
376 val thm = DISCH ant (SPECL cvs(UNDISCH(SPECL vs th)))
379 val RED = RED_WHERE (last vs) (mk_imp(ant,cncl))
380 val tacs = TACS (last vs) ant
437 in let val (ant,conseq) = dest_imp rule
439 val ith = DISCH ant (SPECL cvs (UNDISCH (SPECL vs th)))