slotosch [Fri, 25 Apr 1997 15:31:51 +0200] rev 3058
changed Domain->Dom for SML/NJ
wenzelm [Fri, 25 Apr 1997 15:24:07 +0200] rev 3057
removed -c option;
wenzelm [Fri, 25 Apr 1997 15:18:58 +0200] rev 3056
removed -c option;
wenzelm [Fri, 25 Apr 1997 15:10:52 +0200] rev 3055
removed COPYDB flag;
wenzelm [Fri, 25 Apr 1997 15:08:52 +0200] rev 3054
removed -c option;
wenzelm [Fri, 25 Apr 1997 15:08:25 +0200] rev 3053
obsolete;
wenzelm [Fri, 25 Apr 1997 15:06:21 +0200] rev 3052
no longer forces default;
wenzelm [Fri, 25 Apr 1997 14:12:33 +0200] rev 3051
misc tuning;
oheimb [Fri, 25 Apr 1997 11:11:52 +0200] rev 3050
removed one blank at end of line 37
wenzelm [Thu, 24 Apr 1997 19:47:53 +0200] rev 3049
refer to SOME, NONE on top-level;
wenzelm [Thu, 24 Apr 1997 19:46:24 +0200] rev 3048
adapted for 1.09.27 (and later);
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);
wenzelm [Thu, 24 Apr 1997 19:41:00 +0200] rev 3046
adapted to SML/NJ 1.09.27;
minor cleanup;
nipkow [Thu, 24 Apr 1997 19:08:32 +0200] rev 3045
Added 'induct_tac'
nipkow [Thu, 24 Apr 1997 18:51:14 +0200] rev 3044
Updates because nat_ind_tac no longer appends "1" to the ind.var.
wenzelm [Thu, 24 Apr 1997 18:44:32 +0200] rev 3043
removed space;
nipkow [Thu, 24 Apr 1997 18:38:30 +0200] rev 3042
induct_tac
mueller [Thu, 24 Apr 1997 18:07:35 +0200] rev 3041
expandshort
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...
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.
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