[isabelle-dev] NEWS: cases from goals

[Makarius]

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 
now.

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.


 	Makarius