merged

redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min

remove some uses of Int.succ and Int.pred

removed unused lemmas

remove redundant syntax declaration

use 'induct arbitrary' instead of 'rule_format' attribute

declare simp rules immediately, instead of using 'declare' commands

declare word_of_int_{0,1} [simp], for consistency with word_of_int_bin

be explicit about Finite_Set.fold

dropped fact whose names clash with corresponding facts on canonical fold

prefer canonical fold on lists

be explicit about Finite_Set.fold

incorporated More_Set and More_List into the Main body -- to be consolidated later

moved theorem requiring multisets from More_List to Multiset

NEWS: unavoidable fact renames

dropped disfruitful `constant signatures`

moved various set operations to theory Set (resp. Product_Type)

dropped Executable_Set wrapper theory

updated certificate

NEWS: `set` is now a proper type constructor

dropped references to obsolete facts `mem_def` and `Collect_def`

dropped references to obsolete facts `mem_def_raw` and `Collect_def_raw`

adjusted to set/pred distinction by means of type constructor `set`

treatment of type constructor `set`

executable intervals

`set` is now a proper type constructor

tuned layout

reduced to a compatibility layer

added setup for executable code

moved `sublists` to theory Enum