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

commented out examples which choke on strict set/pred distinction

explicitly spelt out proof of equivariance avoids problem with automation due to type constructor `set`

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

dropped references to obsolete fact `mem_def`

dropped obsolete lemma member_set

dropped obsolete code equation for Id

tuned proofs

generalized type signature to permit overloading on `set`

added monad instance for `set`

enum type class instance for `set`; dropped misfitting code lemma for trancl

finite type class instance for `set`

treatment of type constructor `set`

lattice type class instances for `set`; added code lemma for Set.bind

`set` is now a proper type constructor; added operation for set monad

simplify some proofs

remove redundant lemma word_sub_def

add lemmas bin_cat_zero and bin_split_zero

more uses of 'induct arbitrary'

use 'induct arbitrary' instead of universal quantifiers

remove two conflicting simp rules for 'number_of (number_of _)' pattern

add lemma bin_nth_minus1

removed killed encoding from example

updated docs

killed "guard@?" encodings -- they were found to be unsound

extend previous optimizations to guard-based encodings