Re: [isabelle] Immediate target breaks 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

According to my understanding of loc_begin in src/Pure/Isar/toplevel.ML,
this is the implemented behaviour.  But I doubt it's intended to work
this way.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.