Re: [isabelle-dev] Shadowing of theorem names in locales

[Johannes Hölzl]

Am Sonntag, den 07.10.2012, 18:06 +0200 schrieb Lars Noschinski:
 On 07.10.2012 09:37, Florian Haftmann wrote:
  Hi all,
 
  currently, theorem names in locales can be shadowed (given that
  declarations are in different theories, otherwise the foundation level
  would reject the declaration since the two foundation theorems would
  have the same name).
 
  After some pondering I would argue that this should be forbidden:
  * (Complete) shadowing is a constant source of confusion.
  * Global interpretations are impossible then, since they would result in
  two global theorems with the same name.
 
  Any comments?
 
 How would this interact with sublocale? If two (unrelated) locales 
 contain a lemma with the same name, can I still establish a sublocale 
 relation?
 
-- Lars

You are forced to give a name to the subplocale interpretation:

  sublocale L1  NAME!: L2

but then it should work.

 - Johannes



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] typedef (open) legacy

[Brian Huffman]

On Fri, Oct 5, 2012 at 10:37 AM, Makarius makar...@sketis.net wrote:
 On Thu, 4 Oct 2012, Brian Huffman wrote:

 I was reluctant to support closed type definitions at all in HOLCF's
 cpodef and friends, preferring to make (open) the default behavior; but in
 the end I decided it was more important to make the input syntax consistent
 with typedef. I would be more than happy to remove this feature from the
 HOLCF packages if typedef will be changed to match.

 Do you want to make the first move to remove the (open) option from the
 HOLCF cpodef packages?  I will later follow trimming down HOL typedef --
 there are a few more fine points on my list to iron out there once the set
 defs are gone. Alternatively, I can take do it for 'typdef' packages
 simultaneously.

Hi Makarius,

I have a changeset that removes the set-definition features from the
{cpo,pcpo,domain}def commands in HOLCF, and it checks successfully on
testboard.

http://isabelle.in.tum.de/testboard/Isabelle/rev/a093798fa71b

Should I go ahead and push this changeset to the current tip?

- Brian


 Before doing anything on the packages, we should make another round through
 the visible universe of theories to eliminate the last uses of the legacy
 mode.


 Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev