1999-07-27 paulson [Tue, 27 Jul 1999 10:29:46 +0200] rev 7087
tidied
src/HOL/Sum.ML

1999-07-26 paulson [Mon, 26 Jul 1999 16:32:23 +0200] rev 7086
expandshort
src/HOL/Integ/IntDiv.ML src/HOL/Integ/NatBin.ML

1999-07-26 paulson [Mon, 26 Jul 1999 16:30:50 +0200] rev 7085
HOL/ex/Tarski: new example by Florian Kammueller
src/HOL/IsaMakefile src/HOL/ex/ROOT.ML src/HOL/ex/Tarski.ML src/HOL/ex/Tarski.thy

1999-07-26 paulson [Mon, 26 Jul 1999 16:29:59 +0200] rev 7084
new facts about binomials
src/HOL/Power.ML

1999-07-26 paulson [Mon, 26 Jul 1999 16:29:38 +0200] rev 7083
three new theorems
src/HOL/Relation.ML

1999-07-26 paulson [Mon, 26 Jul 1999 16:08:15 +0200] rev 7082
new cancellation laws
src/HOL/Divides.ML

1999-07-26 paulson [Mon, 26 Jul 1999 10:34:54 +0200] rev 7081
tidied
src/HOL/Integ/Int.ML

1999-07-23 paulson [Fri, 23 Jul 1999 17:49:35 +0200] rev 7080
new simprocs assoc_fold and combine_coeff
src/HOL/Integ/bin_simprocs.ML

1999-07-23 paulson [Fri, 23 Jul 1999 17:31:51 +0200] rev 7079
removed the combine_coeff simproc because linear arith does not handle
coefficients yet
src/HOL/UNITY/Lift.ML

1999-07-23 paulson [Fri, 23 Jul 1999 17:30:27 +0200] rev 7078
now using correctly-typed constants from HOLogic
src/HOL/Tools/numeral_syntax.ML