Re: [isabelle] Controlling the simplification steps

On 16.09.2015 17:24, Thomas Genet wrote:
> The rewrite proof method does not seem to be part of Isabelle2014 that I
> use with my students, but subst is! I'll get by with it.

Indeed, "rewrite" is only part of Isabelle since 2015.

>> Note that this isn't really "step by step simplification", as the
>> simplification of arithmetic expressions takes more then a single step.
> Yes but this is exactly what I want to highlight.

I guessed so ;)

  -- Lars

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