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