nipkow [Thu, 24 Apr 1997 17:59:55 +0200] rev 3037
rename_params_rule used to check if the new name clashed with a free name in
the whole goal state. Now checks only the subgoal concerned.
mueller [Thu, 24 Apr 1997 17:51:27 +0200] rev 3036
deleted definitions for blift and plift
mueller [Thu, 24 Apr 1997 17:50:34 +0200] rev 3035
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
mueller [Thu, 24 Apr 1997 17:40:30 +0200] rev 3034
added liftpair definition
mueller [Thu, 24 Apr 1997 17:38:33 +0200] rev 3033
only in comments
mueller [Thu, 24 Apr 1997 17:35:47 +0200] rev 3032
minor changes due to more powerful continuity check in Lift3.ML
mueller [Thu, 24 Apr 1997 17:04:07 +0200] rev 3031
added some comments;
paulson [Thu, 24 Apr 1997 11:21:46 +0200] rev 3030
Addition of printed tracing. Also some tidying
paulson [Thu, 24 Apr 1997 11:20:56 +0200] rev 3029
A bit of tidying
oheimb [Thu, 24 Apr 1997 10:40:01 +0200] rev 3028
added dependencies on ax_ops/*.ML and domain/*.ML