Re: [isabelle] RC2 for testing; Toplevel.timing has no affect anymore



On 10/14/2013 12:22 PM, Makarius wrote:
The following user-space attribute definition defines something that is
close to the discontinued blast_trace declaration...

Here is also a slightly more elaborate version with argument parser...

A rose by a different name is still a rose. Thanks a lot.

It's also not about proving the theorem. It's about learning something from the blast method. I allocate a few minutes to look at the HOL.impCE that it lists in the details.

Blast is a slightly more sophisticated version from the basic Classical Reasoner. The latter is definitely worth learning, using its fine documentation in the isar-ref manual and its ML sources.

I believe you, but fine documentation generally works best in conjunction with or preceded by the study of a fine textbook.

This looks like a good companion to isar-ref: Structural Proof Theory, by Negri and von Plato.

http://www.helsinki.fi/~negri/ptforum.html

But this free one answered a few questions I had from me just browsing through it to see if it's what I was looking for: Logic for Computer Science, by Reeves & Clarke.

http://www.cs.waikato.ac.nz/~stever/LCS.html

Regards,
GB




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