2000-05-05 nipkow [Fri, 05 May 2000 12:51:33 +0200] rev 8797
Added AVL
src/HOL/IsaMakefile src/HOL/ex/AVL.ML src/HOL/ex/AVL.thy src/HOL/ex/ROOT.ML

2000-05-04 paulson [Thu, 04 May 2000 18:40:57 +0200] rev 8796
if_weak_cong should make linear arithmetic faster
src/HOL/Integ/IntArith.ML

2000-05-04 paulson [Thu, 04 May 2000 18:39:51 +0200] rev 8795
a safer way of proving literal equalities
src/HOL/Integ/NatBin.ML

2000-05-04 paulson [Thu, 04 May 2000 15:17:41 +0200] rev 8794
from Suc...Suc to #m
src/HOL/ex/Primrec.ML

2000-05-04 paulson [Thu, 04 May 2000 15:16:46 +0200] rev 8793
of course it should use Main
src/HOL/Quot/NPAIR.thy

2000-05-04 paulson [Thu, 04 May 2000 15:16:18 +0200] rev 8792
new lemmas concerning powers and #mmm
src/HOL/Integ/NatBin.ML

2000-05-04 paulson [Thu, 04 May 2000 15:15:37 +0200] rev 8791
changed 2 to #2
src/HOL/Hoare/Arith2.ML src/HOL/Hoare/Arith2.thy src/HOL/Hoare/Examples.ML src/HOL/IMPP/EvenOdd.ML src/HOL/IMPP/EvenOdd.thy src/HOL/Quot/FRACT.ML

2000-05-04 paulson [Thu, 04 May 2000 15:14:56 +0200] rev 8790
Suc 0 -> 1
src/HOL/Univ.ML

2000-05-04 paulson [Thu, 04 May 2000 15:14:44 +0200] rev 8789
card_Pow is no longer a default simprule because it uses unary 2
src/HOL/Finite.ML

2000-05-04 paulson [Thu, 04 May 2000 12:29:18 +0200] rev 8788
simprocs
NEWS