Stream: Beginner Questions

Topic: Refer to theorems introduced by sublocale


view this post on Zulip Lukas Stevens (Feb 12 2021 at 10:30):

How does one refer to theorems introduced by sublocale, e.g. see the following example:

theory Scratch imports Main
begin

axiomatization P :: "'a ⇒ bool"

locale foo =
  fixes A :: "'a set"
begin

lemma bar: "X ⊆ A ⟹ P X"
  sorry

end

locale bar
begin

sublocale foo UNIV .

thm bar
end
print_locale! bar (* notes the theorem bar in the locale bar *)
thm bar.bar (* Does not work *)

end

view this post on Zulip Lukas Stevens (Feb 12 2021 at 10:40):

Seems to be answered in this thread: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-May/msg00067.html


Last updated: Mar 28 2024 at 20:16 UTC