search

jrh13 / hol-light

The HOL Light theorem prover
Other
435 stars 79 forks source link

Remove dead code. #56

Closed blynn closed 4 years ago

blynn commented 4 years ago

DISCH_TAC already handles negation so the removed line is superfluous.

I tested this change by executing:

ITAUT a ==> ~(~a)