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.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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