Re: [isabelle] I want to print axiom info (sledgeH error at end)
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