Re: [isabelle] Attributes consumes and case_conclusion ignores unnamed context

On Fri, 26 Oct 2012, Andreas Lochbihler wrote:

In Isabelle2012 and the current development version (ID 3259ea7a52af), the attributes consumes and case_conclusion do not correctly adjust the positions of assumptions. Here's a small example:

context fixes p :: nat assumes "p > 0"

coinductive foo where
 p: "foo p"
| Suc: "foo n ==> foo (Suc n)"

inductive bar where
 p: "bar p"
| Suc: "bar n ==> bar (Suc n)"


Apparently, coinduct tries to define the short-hands for the case conclusions by unifying with the coinduction hypothesis.

After several years of "localizing" most definitional packages to work with locale, class, interpretation targets, we now have stage two of nested context localization starting with the Isabelle2012 release.

I will make an effort when converging towards the coming release to sort out the issues that have been accumulated in the past few months. It will probably take several release cycles until most packages work again after introducing this new feature last winter.


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