Re: [isabelle] question about Simplifier.rewrite


try invoking the simplifier with (simp cong: if_cong)

By default, the simplifier uses thm weak_if_cong as congruence rule for
if, which prevents it from simplifying inside if expressions.


On Mi, 2016-10-26 at 16:30 +0300, Iulia Dragomir wrote:
> Hello
> I have a problem with Simplifier.rewrite which simplifies the
> expression
> (1::real) = (2::real) within some simple term, but not in a more
> complex
> term. Since the complex term is quite involved, the actual questions
> are
> in the attached file, which also contains the term.
> Any help is greatly appreciated.
> Best regards,
> Iulia Dragomir

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