Jakub Kądziołka (Jan 16 2021 at 20:18): Jakub Kądziołka (Jan 16 2021 at 20:18):There are two definitions for prime - one in HOL-Computational_Algebra.Factorial_Ring, and one in HOL-Algebra.Divisibility. When I import both HOL-Number_Theory and HOL-Algebra into a theory (regardless of the order), the latter shadows the former. Thus, if I want to refer to primality of integers, I need to use the full Factorial_Ring.prime. What's the best way to instruct Isabelle to default to Factorial_Ring.prime in my theory?
Manuel Eberl (Jan 16 2021 at 21:08):no idea if there is one
Manuel Eberl (Jan 16 2021 at 21:09):that is a long-standing problem with a number of things
Manuel Eberl (Jan 16 2021 at 21:09):I guess you can do hide_const (open) Divisibility.prime
Manuel Eberl (Jan 16 2021 at 21:10):then you have to spell out Divisibility.prime whenever you want to refer to that
Jakub Kądziołka (Jan 16 2021 at 23:01):Ah, thanks. That's satisfactory to me, as I'm not using Divisibility.prime in particular
Last updated: Dec 21 2024 at 16:20 UTC