Lines Matching defs:b1
288 val imp_thm_conj = prove (``!b1 c1 b2 c2. (b1 ==> c1) ==>
290 (b1 /\ b2) ==>
292 val imp_thm_disj = prove (``!b1 c1 b2 c2. (b1 ==> c1) ==>
294 (b1 \/ b2) ==>
297 val imp_thm_forall = prove (``(!x. (b1 x ==> b2 x)) ==> ((!x. b1 x) ==> (!x. b2 x))``,
352 val (b1,b2) = dest_conj t;
353 val thm1 = DEPTH_STRENGTHEN_CONV conv b1;
356 val (b1,c1) = dest_imp (concl thm1);
358 val thm3 = ISPECL [b1,c1,b2,c2] imp_thm_conj;
366 val (b1,b2) = dest_disj t;
367 val thm1 = DEPTH_STRENGTHEN_CONV conv b1;
370 val (b1,c1) = dest_imp (concl thm1);
372 val thm3 = ISPECL [b1,c1,b2,c2] imp_thm_disj;