[isabelle-dev] NEWS

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Mon Dec 26 17:33:29 CET 2011

'set' is now a proper type constructor.  Definitions mem_def and
Collect_def have disappeared.  INCOMPATIBILITY, rephrase sets S used as
predicates by `%x. x : S` and predicates P used as sets by `{x. P x}`.
For typical proofs, it is often sufficent to prune any tinkering with
former theorems mem_def and Collect_def.


This was just the first step, further coming soon
Do not expect stability before this list has boilt down.

The expected time until the next release hopefully is long enough to
exhibit any minor wart which might have been hidden so far.

Merry Christmas,



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20111226/848216ce/attachment.asc>

More information about the isabelle-dev mailing list