[isabelle-dev] NEWS: cases from goals
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