On 10/14/2013 8:28 AM, Makarius wrote:
Here is a clarified NEWS entry for the release... The same timing information is shown in the extended tooltip of the command keyword, when hovering the mouse over it while the CONTROL or COMMAND modifier is pressed. Does that address all problems and confusions?
Is this supposed to be working for the RC2 release or the next release? All I get in the tooltip when I hover over a "apply" is `command "apply"`. If I can easily see timing for individual "apply" commands, that's great.
It would be nice to have the "using[[blast_trace]]" back.I've rarely used blast, or so I thought, but now that I see that auto calls it a lot, I see I've been using it a lot all along.
You say the blast trace is not meant for user consumption, but I'm using it.The problem with using the global setup for blast trace is that it causes other parts of my THY to "go purple" and stay that way. I could leave a "using[[blast_trace]]" in the file, for various purposes, but I can't do that with "Config.put_global Blast.stats true."
I attach a screenshot that shows I'm using blast trace to learn from it. I try to learn little things here and there as I have time. In this case, I was just looking at the simple goal "((C ==> True) ==> C) ==> B & A ==> C" that gets left over from "simp", and the hints that the blast trace was giving me.
It's not even about figuring out exactly what the blast method is doing. In this case, I saw that "(C ==> True) ==> C) == Trueprop C", so I messed around with that some. There's always different routes to follow.
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 trace the teacher.png
Description: PNG image