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:
> I have a problem with Simplifier.rewrite which simplifies the
> (1::real) = (2::real) within some simple term, but not in a more
> term. Since the complex term is quite involved, the actual questions
> 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