Re: [isabelle] Unexpected assumptions in nested contexts

Hi Lars,

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
IPD Snelting

Dr. Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at
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 MHonArc.