Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Duplicate fact declaration "RBT.color.simps" v...

Email Gateway (Aug 14 2020 at 13:32):

From: Tobias Nipkow <nipkow@in.tum.de>
If I declare both a datatype and a function of the same name t in the same
theory, I get

Duplicate fact declaration "t.simps" vs. "t.simps"

because both commands declare a fact collection of that name. Command hide_fact
doesn't help. Any way around this? Maybe witn some ML name space magic?

Thanks
Tobias
smime.p7s

Email Gateway (Aug 14 2020 at 13:52):

From: Peter Lammich <lammich@in.tum.de>
datatype t = FOO | BAR

setup ‹Sign.mandatory_path "foo"›
fun t :: "nat ⇒ nat" where "t x = Suc x"
setup ‹Sign.parent_path›

thm t.simps
thm foo.t.simps

Email Gateway (Aug 14 2020 at 13:58):

From: Peter Lammich <lammich@in.tum.de>
And here the properly localised version:

datatype t = FOO | BAR

context begin
local_setup ‹Local_Theory.map_background_naming
(Name_Space.mandatory_path "foo")›
fun t :: "nat ⇒ nat" where "t x = Suc x"
end

thm t.simps
thm foo.t.simps

Last updated: Nov 03 2025 at 20:24 UTC