[isabelle-dev] NEWS: cases from goals

[Larry Paulson]

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

Larry

> On 26 Jun 2015, at 23:46, Makarius <makarius at 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev