[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110824/4d55309e/attachment.sig>