Re: [isabelle] Isabelle_17-Jan-2013 scala code export changes



Dear Cornelius,

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
>> sledgehammer_params[isar_proof=true]
>> 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.

Cheers,

Jasmin






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