On 08/23/2011 01:51 PM, Lawrence Paulson wrote:
I'm starting to have doubts about this entire procedure.
I thought the plan was to get these theories (particularly in the
AFP) into a state where they no longer dependent on confusing sets
with predicates so that they would work with either version of
Isabelle.
Only where this is possible. The purpose of all this work is to see
where it is not possible and find out why. After all, these issues may
point to difficulties that users will later experience with the change
as well.
I'm not sure that's possible. I got DataRefinementIBP
working with the set-version, but now it doesn't work with the
standard version. For one thing, it needs a class declaration for
type set, which obviously cannot work with the standard version,
Shouldn't one remove quite a bit of duplication first? The classes
distributive_complete_lattice and complete_boolean_algebra are now part
of HOL (the former as complete_distrib_lattice) (see the FIXME). The set
instances for those should be in/go into Florian's HOL repository as well...
(but maybe you already did this???)
but
other proofs also fail to work with the standard version.
I'd like to (and others probably too) look at those proofs. Is there
anything fundamental hidden there???
Can you send me a bundle of your changes, so that I can put them on the
web for people to look at?
- hg ci # commit your changes locally
- hg bundle SOME_FILENAME http://afp.hg.sourceforge.net/hgweb/afp/afp/
- send me the file SOME_FILENAME, created in the previous step
The second command will produce a file which contains all your
changesets that are not in the central afp repos (i.e., your new changes).
I'll put it up somewhere where people can look at it...
Alex
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
