# [isabelle] simplification at the ML level

Hello,
I woud like to simplify goals having the following pattern : "X ==> False" .
Like for example simplifying
¬ ( (a /= b) \/ (f a = b)) ==> False
to
(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 ?

` Another problem I'm running into is that I want to simplify goal
``without implicitly applying assumption too. For example I would like
``to get
`"X ==> X" from "~~ X ==> ~~X"

`At the proof general level, using "simp" is too strong and finishs the
``proof in 1 step. Using "simp (no_asm)" only simplifies the right hand
``side which is not what I want too. I'm maybe confused by the term
``"assumption" sometimes refering to the hypothesis, sometimes refering
``to the "assumption" tactic.
`And what about that at the ML level ?
Thanks for your help,
Clément

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*