Change the definition of "is_Some" to use an existential.
Add "as ident(H)" to the "case_bool_decide" tactic.
Misc updates to the prelude.
Type classes for finite and countable types.
Update of new memory model.

Most important changes:
* Indeterminacy and pointer fragments on the level of bits, instead of bytes.
* More simple axiomatization of integers, now we use plain [Z]s together with
  predicates to capture overflow etc.
* Remove non-deterministic encoding of values as memory values.
* Construction of the actual memory