[isabelle-dev] Shadowing of theorem names in locales
makarius at sketis.net
Fri Nov 16 15:00:52 CET 2012
On Thu, 11 Oct 2012, Johannes Hölzl wrote:
> HOL-Probability (in Isabelle/bb5db3d1d6dd) and
> Ordinary_Differential_Equations (in AFP/e9fa38f86b76) work now with this
> A surprising change is found in Markov_Models:
> We get an error when an assumption has the same name as a fact in the
> locale loc
> lemma X: "True" ..
> lemma assumes X: "X" shows "True"
> ^- raises "Duplicate fact declaration "local.X" vs. "local.X""
> Is this easily avoidable? I think this might confuse people and add a
> maintenance burden when one adds a fact to a locale with a popular name.
It is a consequence of handling the local fact name space in a fully
authentic way. In the conversions I had done earlier, there were a few
situations with duplicate assumptions of a long statement, so I just
renamed them apart.
More information about the isabelle-dev