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 <><
Description: This is a digitally signed message part.