I think I really like how drule and drule_all work, but is there something that walks the middle road? I mean drule only discharges one condition; and drule_all needs all conditions to be discharged. It would be nice to have a drule that discharges as many as possible and leave the rest as implicants.
Also it appears that drule_all does not check if the theorem is proved and leaves ``P ==> P`` as a goal. Haitao
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
