Complete Redesign of Theory, main points are:
Complete Redesign of Theory, main points are:

- Extension of the continuity prover:
  * Lemmas about continuity of flift1 and flift2 are generalized
  * Lemmas about continuity of mixed definitions of HOL and LCF terms generalized
  Pay attention: Sometimes proofs are shorter now!
- a number of new lemmas concerning flift1, flift2, Def and Undef,
  Def_less_is_eq (Def x << y = (Def x = y)) and lemmas characterizing flift1 and flift2
  are added to !simpset
  Pay attention: Sometimes proofs are shorter now!
- added tactic def_tac for eliminating x~=UU in assumptions

MerelyAPseudonym/isabelle,MerelyAPseudonym/isabelle,MerelyAPseudonym/isabelle,MerelyAPseudonym/isabelle,MerelyAPseudonym/isabelle,MerelyAPseudonym/isabelle