Re: [isabelle] Isabelle_17-Jan-2013 scala code export changes
Am 29.01.2013 um 13:50 schrieb Steffen Juilf Smolka:
> On 28.01.2013, at 21:41, "C. Diekmann" <diekmann at in.tum.de> wrote:
>> No major issues, the only broken thing is
>> No big deal …
> Try sledgehammer_params[isar_proofs] instead. The parameter has been renamed.
It has been renamed, but also the underlying implementation has been improved in a number of important ways, including
1. reliable type annotations
2. proof preplay
3. proof compression (see "isar_shrink" in the manual)
4. some support for skolemization (existentials)
and various bug fixes.
The Isar proof generation feature is still experimental, but it's much less so than in 2012. We (= Steffen and I) would be happy to hear from you if you encounter problems or have success stories to share with us.
This archive was generated by a fusion of
Pipermail (Mailman edition) and