[isabelle-dev] NEWS: cases from goals

[Lars Noschinski]

On 30.06.2015 17:42, Makarius wrote:
> Above I am using a new idiom, to name "prems" uniformly in each case.
> This helps to avoid specific names like "1", "2" etc. intrude the
> proof body.  Thus cases may be re-arranged later, without changing all
> the proof cases.
>
> Moreover note, that the above example provides a solution to the
> occasional problem of ?thesis1, ?thesis2, etc. -- which are not
> provided by the system.  It just becomes ?case in each case.
I'd say this is a partial solution: When I have a situation where I need
?thesis1, ?thesis2, etc. then the goals are often very similar to solve
and my proof concludes with "... show ?thesis1 ?thesis ...".

I wonder though, why the goals method is better then the implicit goal1,
goal2, ... cases? Doesn't it lead to more instances of "proof
(initial_method, goals)" -- which I thought is a style you discouraged?

  -- Lars