clasohm [Fri, 22 Apr 1994 21:23:14 +0200] rev 69
renamed theory files
lcp [Thu, 21 Apr 1994 11:28:32 +0200] rev 68
tidied definitions and proofs
lcp [Thu, 21 Apr 1994 11:13:22 +0200] rev 67
HOL/arith.ML/plus_leD1: tidied
nipkow [Tue, 19 Apr 1994 10:50:00 +0200] rev 66
changed defns in hol.thy from = to ==
lcp [Wed, 06 Apr 1994 16:31:06 +0200] rev 65
Now simplifies before the induction
nipkow [Wed, 30 Mar 1994 10:00:23 +0200] rev 64
@ now associates to the right, just like #, in order to avoid loss of
parentheses due to pretty printer.
nipkow [Sun, 27 Mar 1994 16:43:06 +0200] rev 63
Added some sums.
nipkow [Sun, 27 Mar 1994 12:36:39 +0200] rev 62
integrated permutative rewriting
nipkow [Tue, 22 Mar 1994 19:55:29 +0100] rev 61
used new field "simps" of Datatype
nipkow [Tue, 22 Mar 1994 19:54:55 +0100] rev 60
new field "simps" added