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
patch.
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:
locale loc
begin
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.
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
