Having 'a set back

From Isabelle Community Wiki
Jump to: navigation, search

(Re-)introducing set as a type constructor rather than as a mere type abbreviation.


The historical critical changesets:

hg diff -r e8cc166ba123 -r 1d963bfd4a1b
hg diff -r ba4ec2d16ed0 -r f73797756637


issue dealt with by
drop theory Cset (naive version and quotient version) done
mark _apply rules for pointwise operations on functions as [code] done by Florian
tuning of list fold combinators done
re-checking of pred_to_set declarations done
provide theories Dlist_Set, Mapping_Set, etc. Ondřej
backport theory Set_Algebras to type classes done
code generator preprocessing for set comprehensions
reworking of Execute.thy in CoreC++ done by Andreas
refine enum type classes to use sets rather than lists not possible due to function instances which require ordering of elements; cleaned up theory Enum.thy nonetheless