[isabelle-dev] NEWS

[Makarius]

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