Thu, 24 Apr 1997 17:51:27 +0200 deleted definitions for blift and plift
mueller [Thu, 24 Apr 1997 17:51:27 +0200] rev 3036
deleted definitions for blift and plift
Thu, 24 Apr 1997 17:50:34 +0200 Complete Redesign of Theory, main points are:
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
Thu, 24 Apr 1997 17:40:30 +0200 added liftpair definition
mueller [Thu, 24 Apr 1997 17:40:30 +0200] rev 3034
added liftpair definition
Thu, 24 Apr 1997 17:38:33 +0200 only in comments
mueller [Thu, 24 Apr 1997 17:38:33 +0200] rev 3033
only in comments
Thu, 24 Apr 1997 17:35:47 +0200 minor changes due to more powerful continuity check in Lift3.ML
mueller [Thu, 24 Apr 1997 17:35:47 +0200] rev 3032
minor changes due to more powerful continuity check in Lift3.ML
Thu, 24 Apr 1997 17:04:07 +0200 added some comments;
mueller [Thu, 24 Apr 1997 17:04:07 +0200] rev 3031
added some comments;
(0) -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip