Re: [isabelle] Converting apply-style induction to Structured Isar

2011/3/31 Johannes Hölzl <hoelzl at>:
> - If you use "case" with the method "induct" the thesis is not
>  named ?thesis but ?case, the facts are named after the case name (look
> at Isabelle / Show me / Facts) :

This really made my day -- I have been craving for such a feature for
very long :-)
Thank you for all your suggestions and solutions - it sped up my
learning process a lot!


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.