[isabelle] Implicit structure argument


I have problems declaring something as "(structure)", when it is not a
locale parameter (Isabelle2012 is used). Take the following example:

definition adj :: "'a set ⇒ 'a ⇒ 'a ⇒ bool" ("_ →ı _" [100,100] 40) where "
  adj G v w ≡ v ∈ G ∧ v = w"

locale Foo =
  fixes G :: "'a set" (structure)

locale Bar =
  fixes s :: "'a"
definition "s_G = {s}"

sublocale Bar ⊆ Foo s_G by unfold_locales

In the context 'Bar' I'd like to use "v → w", but I can't as s_G is not
marked as an implicit structure. I then tried (in context Bar)

notation s_G (structure)

From reading the documentation, this should be legal, but it yields:

*** Bad mixfix declaration for "local.s_G"

I appreciate any useful hints to make s_G the implicit structure argument.


René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift

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