Re: [isabelle] simplification at the ML level
On Thursday 20 April 2006 17:44, Clement.Hurlin at esial.uhp-nancy.fr wrote:
> I woud like to simplify goals having the following pattern : "X ==>
> False" . Like for example simplifying
> ¬ ( (a /= b) \/ (f a = b)) ==> False
> (a = b /\ f b /= b) ==> False
> (at the ML level) But the Simp_tac tactic fails, I guess because it
> works from bottom to up.
> What should I use ?
if you just need CNF conversion, I suggest you take a look at the existing
code in HOL/Tools/cnf_funcs.ML, and also in HOL/Tools/meson.ML.
This archive was generated by a fusion of
Pipermail (Mailman edition) and