[isabelle-dev] NEWS

[Florian Haftmann]

'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
(https://isabelle.in.tum.de/isanotes/index.php/Having_'a_set_back%23Roaring_ahead).
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,
	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://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20111226/848216ce/attachment.asc>