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.

Overview

The historical critical changesets:

http://isabelle.in.tum.de/reports/Isabelle/shortlog/d889d57445dc
hg diff -r e8cc166ba123 -r 1d963bfd4a1b
http://afp.hg.sourceforge.net/hgweb/afp/afp/shortlog/f73797756637
hg diff -r ba4ec2d16ed0 -r f73797756637

Polishing

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