* Integrated image HOL-Complex with HOL. Entry points Main.thy and Complex_Main.thy remain as they are.
* New image HOL-Plain provides a minimal HOL with the most important tools available (inductive, datatype, primrec, ...). By convention the corresponding theory Plain should be ancestor of every further (library) theory. Florian -------------- next part -------------- A non-text attachment was scrubbed... Name: florian.haftmann.vcf Type: text/x-vcard Size: 654 bytes Desc: not available Url : https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20080701/d486f8d4/attachment.vcf -------------- next part -------------- A non-text attachment was scrubbed... Name: signature.asc Type: application/pgp-signature Size: 185 bytes Desc: OpenPGP digital signature Url : https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20080701/d486f8d4/attachment.pgp