Isabelle2013-1-RC1 adaptation
regenerated
fixed import
new lemma about big Union and set comprehension, which is currently needed in Sandbox/b.thy
deleted ll22, as it is equivalent with something from the library (Isabelle2013-1-RC1 nicely points out such situations)
did one proof manually which is no longer as easy as it used to be, given the new big operators in Isabelle2013-1-RC1
minor Isabelle2013-1-RC1 cleanup
Isabelle2013-1-RC1: removed some unused facts in metis proofs
replaced redundant lemma l32 by runiq_alt
new big Union operator precedence
replaced redundant lemma ll10 by trivial_singleton
using new Isabelle2013-1-RC1 lattice library; minor cleanup of unused steps