Thu, 24 Apr 1997 19:46:05 +0200 open General (type option is in Option in the newer versions, but always
wenzelm [Thu, 24 Apr 1997 19:46:05 +0200] rev 3047
open General (type option is in Option in the newer versions, but always the top-level);
Thu, 24 Apr 1997 19:41:00 +0200 adapted to SML/NJ 1.09.27;
wenzelm [Thu, 24 Apr 1997 19:41:00 +0200] rev 3046
adapted to SML/NJ 1.09.27; minor cleanup;
Thu, 24 Apr 1997 19:08:32 +0200 Added 'induct_tac'
nipkow [Thu, 24 Apr 1997 19:08:32 +0200] rev 3045
Added 'induct_tac'
Thu, 24 Apr 1997 18:51:14 +0200 Updates because nat_ind_tac no longer appends "1" to the ind.var.
nipkow [Thu, 24 Apr 1997 18:51:14 +0200] rev 3044
Updates because nat_ind_tac no longer appends "1" to the ind.var.
Thu, 24 Apr 1997 18:44:32 +0200 removed space;
wenzelm [Thu, 24 Apr 1997 18:44:32 +0200] rev 3043
removed space;
Thu, 24 Apr 1997 18:38:30 +0200 induct_tac
nipkow [Thu, 24 Apr 1997 18:38:30 +0200] rev 3042
induct_tac
Thu, 24 Apr 1997 18:07:35 +0200 expandshort
mueller [Thu, 24 Apr 1997 18:07:35 +0200] rev 3041
expandshort
Thu, 24 Apr 1997 18:06:46 +0200 Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow [Thu, 24 Apr 1997 18:06:46 +0200] rev 3040
Introduced a generic "induct_tac" which picks up the right induction scheme automatically. Also changed nat_ind_tac, which does no longer append a "1" to the name of the induction variable. This caused some changes...
Thu, 24 Apr 1997 18:03:23 +0200 get_thydata accesses the second component of the data field. This component
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.
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.
(0) -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip