[isabelle-dev] NEWS

[Florian Haftmann]

Sets are now reasonably executable in HOL-Main.  At the moment this
demands to include theories More_List and More_Set directly in HOL-Main,
but I will amend this over time.

Volunteers could have a look at the list of open issues:
https://isabelle.in.tum.de/isanotes/index.php/Having_%27a_set_back

With the exception of the last two »maybe« entries (the last being
reallsy doubtful), I consider all of the show stoppers for the next release.

Apart from those already assigned, a few are still awaiting their redeemer:

* drop theory Cset (naive version)

haftmann at scarlatti:/data/tum/isabelle/master$ grep -rIPl Cset src/
contrib/afp
src/HOL/IsaMakefile
src/HOL/Library/ROOT.ML
src/HOL/Library/Cset.thy
src/HOL/Library/Library.thy
src/HOL/Library/List_Cset.thy
src/HOL/Library/Cset_Monad.thy
src/HOL/Library/Dlist_Cset.thy
src/HOL/Quotient_Examples/ROOT.ML
src/HOL/Quotient_Examples/Quotient_Cset.thy
src/HOL/Quotient_Examples/List_Quotient_Cset.thy
contrib/afp/thys/Functional-Automata/ROOT.ML
contrib/afp/thys/Functional-Automata/Execute_Quotient.thy
contrib/afp/thys/Functional-Automata/Execute.thy
contrib/afp/thys/CoreC++/WellForm.thy

It looks like that it is sufficient to move Cset.thy to
Functional-Automata and delete all the other stuff.

* instantiation set :: ("{random, type}") random and other additions

@Lukas?

* restore previous rule declarations:
    * lemma predicate1I [Pure.intro!, intro!]
    * lemma pred_equals_eq [pred_set_conv]
    * lemma pred_subset_eq [pred_set_conv]
and
* mark _apply rules for pointwise operations on functions as [simp]

@Lars?

* provide theories Dlist_Set, RBT_Set (or maybe Mapping_Set), etc.
--> now a joyful little exercise

* backport theory Set_Algebras to type classes
--> now a joyful little exercise

	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://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20111227/eb31773c/attachment.sig>