Re: [isabelle] Fw: term of partial_function body



On 2018-03-29 21:21, Peter Lammich wrote:
>
>     There should be a theorem solve_equation.simps, and its rhs should
>     be the term you are looking for.
>

Ahhh, there is all we need in Isabelle/ML (while a theorem cannot be not
found in Isabele/jEdit for good reasons).

Thanks a lot (saved much time for hacking context.ML) !
>
>
>     Peter
>
Walther



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