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 MHonArc.