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

On 7/17/2012 3:04 AM, Jasmin Blanchette wrote:
...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.) Regards, Jasmin

Okay. If I don't know how to use introduction and elimination rules to replace metis steps, after the initial cheap thrill of a structured proof, it's all kind of the same (though not really, if I'm looking for some hints), and a single-line metis proof takes up less space anyway.

I should get lots of preliminary cheap thrills from using nitpick and sledgehammer, while being able to delay the point at which I have to start thinking, where I get an occasional (or frequent), unexpected result that enlightens me.


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