Sidi Ehmety's port of the fold_set operator and multisets to ZF.
Also, fixes to the cancellation simprocs and a few new standard lemmas.
(* Title: ZF/IMP/Evalb.thy
ID: $Id$
Author: Heiko Loetzbeyer & Robert Sandner, TUM
Copyright 1994 TUM
Dummy theory merely recording dependence
*)
Evalb = Evalb0