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



Hi,

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
begin
  (* ... *)
  sublocale  A "n = 0".
  (* ... *)
  lemma n: "n = 0" sorry
  sublocale  B "n = 0" by (unfold_locales, simp add: n)
  (* ... *)
end

I guess I should be more optimistic.

Greetings,
Joachim


-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

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



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