[isabelle-dev] NEWS: cases from goals

Makarius makarius at sketis.net
Tue Jun 30 00:15:11 CEST 2015

On Fri, 26 Jun 2015, Larry Paulson wrote:

> Multivariate_Analysis/Integration.thy uses goal1 206 times, so this will 
> take a while.

AFP probably has a few thousand.  I did not even check before sorting out 
this old problem from more than 10 years ago.  It could have been 
addressed earlier, then there would have been less work to eliminate it 

Generally, there are more things that can be improved on Isar proofs, 
using the new facilities like 'consider' and 'have' / 'show' with 
eigen-context. Quite often, the elimination of awkward goal42(17) proofs 
actually uses that instead of falling back on the new "goals" method.


More information about the isabelle-dev mailing list