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