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

Reply via email to