Re: [isabelle] Definitions of Superlocale Cannot be Accessed in Assumptions



Hi Julian,

find attached a more minimal example.

> My guess is that this has something to do with the fact that the
> locale "foo" is already interpreted in its most general form as part
> of "baz", so the constants do not get interpreted again when declaring
> "test" can and only be accessed using the prefix "baz" (although the
> parameter "x" is not yet applied there). However, I do not understand
> why they can be accessed in the body of the locale "test", but not
> while declaring its assumptions.

Your suspicion might be true.  Parsing locale specifications is a
notoriously difficult business.  It will need further rounds of
investigation to see what is really going on here.

Cheers,
	Florian

-- 

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

Attachment: Locale_Read.thy
Description: application/extension-thy

Attachment: signature.asc
Description: OpenPGP digital signature



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