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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
