Thu, 24 Mar 1994 13:43:45 +0100 structural induction for strict lists
nipkow [Thu, 24 Mar 1994 13:43:45 +0100] rev 298
structural induction for strict lists
Thu, 24 Mar 1994 13:36:34 +0100 Franz fragen
nipkow [Thu, 24 Mar 1994 13:36:34 +0100] rev 297
Franz fragen
Thu, 24 Mar 1994 13:25:12 +0100 revisions to first Springer draft
lcp [Thu, 24 Mar 1994 13:25:12 +0100] rev 296
revisions to first Springer draft
Wed, 23 Mar 1994 16:56:44 +0100 have broken line
nipkow [Wed, 23 Mar 1994 16:56:44 +0100] rev 295
have broken line
Wed, 23 Mar 1994 15:21:41 +0100 final CADE version
lcp [Wed, 23 Mar 1994 15:21:41 +0100] rev 294
final CADE version
Wed, 23 Mar 1994 13:05:12 +0100 first draft of Springer volume
lcp [Wed, 23 Mar 1994 13:05:12 +0100] rev 293
first draft of Springer volume
Wed, 23 Mar 1994 11:32:21 +0100 first draft of Springer volume
lcp [Wed, 23 Mar 1994 11:32:21 +0100] rev 292
first draft of Springer volume
Wed, 23 Mar 1994 11:10:16 +0100 first draft of Springer volume
lcp [Wed, 23 Mar 1994 11:10:16 +0100] rev 291
first draft of Springer volume
Tue, 22 Mar 1994 12:43:51 +0100 changed "." to "$" and added parentheses to eliminate ambiguity
clasohm [Tue, 22 Mar 1994 12:43:51 +0100] rev 290
changed "." to "$" and added parentheses to eliminate ambiguity
Tue, 22 Mar 1994 12:42:56 +0100 changed "." to "$" to eliminate ambiguity
clasohm [Tue, 22 Mar 1994 12:42:56 +0100] rev 289
changed "." to "$" to eliminate ambiguity
Tue, 22 Mar 1994 08:24:14 +0100 Implemented "ordered rewriting": rules which merely permute variables, such
nipkow [Tue, 22 Mar 1994 08:24:14 +0100] rev 288
Implemented "ordered rewriting": rules which merely permute variables, such as commutativity, are only applied if the term becaomes lexicographically smaller (according to some fixed ordering on the term structure).
Mon, 21 Mar 1994 11:41:41 +0100 first draft of Springer book
lcp [Mon, 21 Mar 1994 11:41:41 +0100] rev 287
first draft of Springer book
Mon, 21 Mar 1994 11:02:57 +0100 first draft of Springer book
lcp [Mon, 21 Mar 1994 11:02:57 +0100] rev 286
first draft of Springer book
Mon, 21 Mar 1994 10:51:28 +0100 first draft of Springer book
lcp [Mon, 21 Mar 1994 10:51:28 +0100] rev 285
first draft of Springer book
Sat, 19 Mar 1994 03:01:25 +0100 First draft of Springer book
lcp [Sat, 19 Mar 1994 03:01:25 +0100] rev 284
First draft of Springer book
Thu, 17 Mar 1994 17:48:37 +0100 new type declaration syntax instead of numbers
lcp [Thu, 17 Mar 1994 17:48:37 +0100] rev 283
new type declaration syntax instead of numbers
Thu, 17 Mar 1994 13:54:50 +0100 FOL/simpdata: tidied
lcp [Thu, 17 Mar 1994 13:54:50 +0100] rev 282
FOL/simpdata: tidied FOL/simpdata/not_rews: moved the law "~(P|Q) <-> ~P & ~Q" from distrib_rews FOL/simpdata/cla_rews: added the law "~(P&Q) <-> ~P | ~Q"
Thu, 17 Mar 1994 13:07:48 +0100 CTT/ex/elim.ML: in the two proofs of Axiom of Choice, changed X-->Y to PROD
lcp [Thu, 17 Mar 1994 13:07:48 +0100] rev 281
CTT/ex/elim.ML: in the two proofs of Axiom of Choice, changed X-->Y to PROD h:X.Y to fix the variable name h:X.
Thu, 17 Mar 1994 12:56:44 +0100 CCL/ccl.ML/po_refl_iff_T: deleted reference to make_iff_T
lcp [Thu, 17 Mar 1994 12:56:44 +0100] rev 280
CCL/ccl.ML/po_refl_iff_T: deleted reference to make_iff_T CCL/ccl.ML/CCL_ss: now includes po_refl RS P_iff_T
Thu, 17 Mar 1994 12:36:58 +0100 Improved layout for inductive defs
lcp [Thu, 17 Mar 1994 12:36:58 +0100] rev 279
Improved layout for inductive defs
Thu, 17 Mar 1994 11:24:31 +0100 adapted type definition to new syntax
clasohm [Thu, 17 Mar 1994 11:24:31 +0100] rev 278
adapted type definition to new syntax
Fri, 04 Mar 1994 12:14:21 +0100 fixed misfeature in Sign.extend: types of consts were read wrt. the new syntax;
wenzelm [Fri, 04 Mar 1994 12:14:21 +0100] rev 277
fixed misfeature in Sign.extend: types of consts were read wrt. the new syntax;
Thu, 03 Mar 1994 17:43:14 +0100 changed "x" to "uu" for implicit name of the
lcp [Thu, 03 Mar 1994 17:43:14 +0100] rev 276
changed "x" to "uu" for implicit name of the dependent type variable
Tue, 01 Mar 1994 17:21:47 +0100 update towards LNCS
nipkow [Tue, 01 Mar 1994 17:21:47 +0100] rev 275
update towards LNCS
Tue, 01 Mar 1994 16:00:53 +0100 deleted a comment
nipkow [Tue, 01 Mar 1994 16:00:53 +0100] rev 274
deleted a comment
Sat, 26 Feb 1994 16:27:45 +0100 *** empty log message ***
nipkow [Sat, 26 Feb 1994 16:27:45 +0100] rev 273
*** empty log message ***
Mon, 21 Feb 1994 14:50:48 +0100 improved explode_tr;
wenzelm [Mon, 21 Feb 1994 14:50:48 +0100] rev 272
improved explode_tr;
Wed, 16 Feb 1994 15:17:15 +0100 minor update because HOL-lemma changed
nipkow [Wed, 16 Feb 1994 15:17:15 +0100] rev 271
minor update because HOL-lemma changed
Wed, 16 Feb 1994 13:56:20 +0100 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp [Wed, 16 Feb 1994 13:56:20 +0100] rev 270
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead instantiate changes the indices of V and W. tactic/cut_inst_tac: new
Wed, 16 Feb 1994 09:22:15 +0100 moved 'unlink ".tmp.ML"' away from 'use ".tmp.ML"' to try to fix a bug with SML
clasohm [Wed, 16 Feb 1994 09:22:15 +0100] rev 269
moved 'unlink ".tmp.ML"' away from 'use ".tmp.ML"' to try to fix a bug with SML
(0) -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip