Re: [isabelle] Failing afp-2015 build



On Tue, 17 Nov 2015, Peter Gammie wrote:

I had in mind to revisit it now-ish, but youâve beaten me to it. The idea was to turn vcg_jackhammer into something case-like, so the larger proofs would look like:

proof vcg_jackhammer
 case (statement_label x y z) then show ?thesis
   < existing apply gloop >
â

We talked about this earlier. I now have time to chase up your pointers. I hoped this would yield the kind of parallelism your âsubgoalâs do now, with the advantage that itâd be more maintainable. Perhaps itâs a wash at this stage.

(Back to this thread, which is not yet closed in all its sub-threads.)

Using the 'subgoal' command of future Isabelle2016 did indeed make a significant difference some months ago. Nonetheless there seems to be room for more efficiency of the basic proof tools used here.

Just from the English, what does "Perhaps itâs a wash at this stage." meand?


	Makarius


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