[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 *)
end

Andreas

--
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
http://pp.info.uni-karlsruhe.de
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.