Re: [isabelle] Unexpected assumptions in nested contexts
Makarius has already fixed this in the development branch, your example works
there. This will also work in the next Isabelle release as expected. For the
moment, you cannot do much about this in Isabelle2012. If you absolutely depend
on this working correct, you could try and switch to the development version,
but this incurs a lot of extra trouble.
Am 28.10.2012 22:13, schrieb Lars Hupel:
(I already posted this several months ago, got no replies, and forgot
about it. I'm sending it again in case there's a solution/workaround
which I've missed. The original thread is at
Nesting two contexts, where the inner context makes assumptions about
fixed variables from the outer context, results in unexpected
all-quantified assumptions. Consider this minimal example:
fixes I :: "'a set"
assumes I: "finite I"
lemma test: "something_about I"
Looking at the fact `test` from outside both contexts with `thm test`, I
(!!I. finite I) ==> ?something_about ?I
Obviously, this fact says something completely different. Am I doing
something wrong here?
Karlsruher Institut für Technologie
Dr. Andreas Lochbihler
Am Fasanengarten 5, Geb. 50.34, Raum 025
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
in der Helmholtz-Gemeinschaft
This archive was generated by a fusion of
Pipermail (Mailman edition) and