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