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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and