Email Gateway (Aug 18 2022 at 17:28): Email Gateway (Aug 18 2022 at 17:28):From: Timothy McKenzie <tjm1983@gmail.com>
On Wed, 30 Mar 2011 21:55:34 Johannes Hölzl wrote:
Did you try Isabelle2011? Of course the type real ^ 'n was not
removed, but for most lemmas the constant names changed.
No, I haven't tried it yet. I keep changing my mind about how
much work it might require to make my project work with
Isabelle2011. Perhaps I should just try it.
Either you rewrite your terms (which is mostly Search &
Replace) or you try to stay with the "real ^ 'n" constants and
use the simplifier to rewrite them at each proof (but I'm not
sure how well this approach works).Alternatively we could try to add the real^'n version of all
changed lemmas back (by specialising the lemmas about
euclidean spaces).
I often think my work would have been simpler if Isabelle2011
existed when I started (in early 2009). As well as the recent
introduction of euclidean_space, the quotient types introduced in
Isabelle2009-2 might have helped if they had existed earlier. But
Isabelle is still improving, so I'll just have to be glad that
these features are available now, for future work.
When we introduced this changes I were not aware of any
existing work using Multivariate_Analysis. Hence we did not
care about backwards compatibility. But we can try to add
compatibility lemmas so you can port your work to the next
Isabelle release. Is your work available anywhere? Is it
possible to take a look at it?
My work is still a work in progress (for a Master's thesis), but
if you want, I could send you off-list the current files, or
perhaps I could try to figure out how to give you at least read-
only access to my subversion repository.
Greetings,
Johannes
Thanks for your help.
Tim
<><
signature.asc
Last updated: Apr 27 2024 at 01:05 UTC