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

ASM_MESON_TAC and MESON_TAC are broken #5

Open dungpa opened 11 years ago

dungpa commented 11 years ago

The consequences are the following erroneous theorems:

Also the messages printed out by these tactics ("solved at...") don't seem to agree with OCaml output.