Thu, 24 Apr 1997 18:00:22 +0200 Main changes are:
mueller [Thu, 24 Apr 1997 18:00:22 +0200] rev 3038
Main changes are: - Lemmas for blift and plift are deleted - added split_tac for If (via If2, as If does not begin with a constant) - added new lemmata relating TT, FF and booleans: Def_bool1, Def_bool2, Def_bool3,Def_bool4 They are added to !simpset, but should not cause difficulties - added lemma andalso_or relating | on booleans and andalso on truth values - deleted If_and_if and andalso from !simpset: Pay attention, may kill your proofs! - added adm lemmas for (f x)~=TT and (f x)~=FF.
Thu, 24 Apr 1997 17:59:55 +0200 rename_params_rule used to check if the new name clashed with a free name in
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.
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
(0) -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip