On Mon, 26 Dec 2011, Florian Haftmann wrote:
'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.
The NEWS entry looks a bit too optimistic. The majority of users after
Isabelle2008 will have to change their theories, and need some more
explicit instructions how to do it sucessfully (e.g. port forwards by
eliminating mem_def/Collect_def before making the actual jump into the new
version).
BTW, ASCII back-quotes have a certain formal status in Isabelle/Isar,
which makes the above use a bit confusing. In plain text explanations,
inner syntax is normally quoted via "..." and outer keywords via '...'
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
