Lukas Stevens (Feb 12 2021 at 10:30): 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
Seems to be answered in this thread: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-May/msg00067.html
Last updated: Dec 21 2024 at 16:20 UTC