Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 19 2022 at 12:10):

From: Joachim Breitner <breitner@kit.edu>
Hi,

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
signature.asc

Last updated: Apr 26 2024 at 01:06 UTC