Re: [isabelle] I want to print axiom info (sledgeH error at end)

Hi Gottfried,

Am 17.07.2012 um 09:00 schrieb Gottfried Barrow:

> If I choose a structured proof, it complains about an unbound schematic variable, as shown in the attached screen shot.

Isar proofs are experimental, as mentioned in the Sledgehammer manual. We have a student currently working on improving them, and he will look into these kinds of issues. Hopefully the next Isabelle release will feature a revamped Isar proof output in Sledgehammer.

Other aspects of Sledgehammer should be more polished. If you run into any bugs with it, please send me an email so I can look into this. (I might otherwise miss bug reports when they hide in lengthy emails on public mailing lists.)



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