'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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
