Re: [isabelle] Calling sublocale A < B in A’s context?


Am Montag, den 21.10.2013, 14:32 +0200 schrieb Joachim Breitner:
> Is there a way to declare a sublocale
> relationship for the current locale form within that locale?

sorry for the noise, Andreas told me that the syntax which I would have
wished for this actually works:

locale C =
  fixes n :: nat
  (* ... *)
  sublocale  A "n = 0".
  (* ... *)
  lemma n: "n = 0" sorry
  sublocale  B "n = 0" by (unfold_locales, simp add: n)
  (* ... *)

I guess I should be more optimistic.


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

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