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"
begin

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

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

end

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.


	Makarius





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