search

jack-pappas / NHol

An implementation of higher-order logic (HOL) in F#. Based on hol-light, Isabelle, and HOL4.
Apache License 2.0
11 stars 4 forks source link

REWRITE_TAC broken #2

Closed domasin closed 11 years ago

domasin commented 11 years ago

REWRITE_TAC seems broken infact proofs that use it can't be solved.

Examples: ABS_SIMP, EXISTS_UNIQUE_THM, EXISTS_UNIQUE_REFL,...

domasin commented 11 years ago

The problem seems to be in the INSTANTIATE function of drule module

jack-pappas commented 11 years ago

Closing the issue because it seems to have been fixed. @domasin Please re-open this issue if you find there are still any issues with INSTANTIATE.