[isabelle] Immediate target breaks unnamed context

According to the Isar-Ref manual (p. 79), immediate target specifications should suspend the current context only for the given command. However, Isabelle apparently fails to restore the current (unnamed) context.

In the following example, I would expect that assumption P in the following example is still available after lemma L, but Isabelle complains that P was unknown. Similar, fixed parameters get lost. Is this a bug or unintended usage of unnamed contexts? Note that I still need to use "end" to close the unnamed context.

locale l = fixes n :: nat

consts P :: bool
context fixes n :: nat assumes P: "P" begin

lemma (in l) L: "True" ..

lemma P': "P" by(rule P) (* Unknown fact P *)
term n (* has type 'a *)


Karlsruher Institut für Technologie
IPD Snelting

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.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 MHonArc.