Multivariate_Analysis/Integration.thy uses goal1 206 times, so this will take a while.
Larry > On 26 Jun 2015, at 23:46, Makarius <makar...@sketis.net> wrote: > > * Proof method "goals" turns the current subgoals into cases within the > context; the conclusion is bound to variable ?case in each case. > > * The undocumented feature of implicit cases goal1, goal2, goal3, etc. > is marked as legacy, and will be removed eventually. Note that proof > method "goals" achieves a similar effect within regular Isar. > > > This refers to c708dafe2220 and d2fbc021a44d. Example updates of oldd proofs > are can be seen in changeset 7e741e22d7fc. > > > Makarius > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
