nipkow [Thu, 24 Apr 1997 18:03:23 +0200] rev 3039
get_thydata accesses the second component of the data field. This component
used to be empty until set at the end of loading an ML file. Now the second
component is already set when the thy file has ben read.
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.
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.