Hi all, > 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???)
concerning Complete_Lattice, of course: http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/893a53a63ba2#l1.7 > 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 confess our infrastructure at the moment is not that good. When there is time, I will allocate an afp_set repository beside the isabelle_set one. I was driven crazy some months ago when I attempted in vain to enable push access. I don't even know what the problem was (authentication, web server configuration, encrpytion) – maybe I wasn't even able to figure out. If someone of the TUM guys knows better, tell me. So the tool of choice would be that each involved in that story to set up his own repositories and publish them by HTTP. Then we can pull each other's changesets. Are there any obstacles? Cheers, Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
