Re: [isabelle] case_names, obtains (par_name), and named local hypotheses
On Thu, 2 Jul 2015, Andreas Lochbihler wrote:
This seems to be a deficiency of the cases method (just like it not
binding ?case to the conclusion).
The cases method never changes the conclusion, so it is just ?thesis.
The extra features of the "induct" family have brought it to the brink of
self-destruction. It is hard to say today what it does and what not. It
needs a major reform.
This archive was generated by a fusion of
Pipermail (Mailman edition) and