1998-10-09 nipkow [Fri, 09 Oct 1998 11:15:39 +0200] rev 5627
added Induct/Multiset*
src/HOL/IsaMakefile

1998-10-09 nipkow [Fri, 09 Oct 1998 11:15:07 +0200] rev 5626
New inductive definition of `card'
src/HOL/Finite.ML src/HOL/Finite.thy

1998-10-09 paulson [Fri, 09 Oct 1998 11:10:59 +0200] rev 5625
polymorphic versions of nat_neq_iff and nat_neqE
src/HOL/Lambda/Eta.ML src/HOL/Lex/RegSet_of_nat_DA.ML src/HOL/Ord.ML src/HOL/UNITY/Channel.ML src/HOL/UNITY/LessThan.ML src/HOL/UNITY/Token.ML

1998-10-08 nipkow [Thu, 08 Oct 1998 11:59:17 +0200] rev 5624
Further improvement of the simplifier.
src/Pure/thm.ML

1998-10-07 nipkow [Wed, 07 Oct 1998 18:17:37 +0200] rev 5623
Tuned simplifier not to re-normalized already normalized terms.
src/Pure/thm.ML

1998-10-07 wenzelm [Wed, 07 Oct 1998 17:51:11 +0200] rev 5622
tuned rm CVS;
Admin/makedist

1998-10-07 nipkow [Wed, 07 Oct 1998 13:21:50 +0200] rev 5621
runs test
doc-src/Tutorial/IsaMakefile

1998-10-07 paulson [Wed, 07 Oct 1998 10:32:00 +0200] rev 5620
tidying and renaming
src/HOL/UNITY/Common.ML src/HOL/UNITY/Comp.ML src/HOL/UNITY/Constrains.ML src/HOL/UNITY/Constrains.thy src/HOL/UNITY/Mutex.ML src/HOL/UNITY/ROOT.ML src/HOL/UNITY/SubstAx.ML src/HOL/UNITY/SubstAx.thy src/HOL/UNITY/Traces.ML src/HOL/UNITY/Traces.thy src/HOL/UNITY/Union.ML src/HOL/UNITY/WFair.ML

1998-10-07 paulson [Wed, 07 Oct 1998 10:31:30 +0200] rev 5619
new theorems
src/HOL/Lex/Prefix.ML

1998-10-07 paulson [Wed, 07 Oct 1998 10:31:07 +0200] rev 5618
tidied
src/HOL/Induct/Acc.ML src/HOL/Induct/LFilter.ML src/HOL/Induct/Simult.ML src/HOL/ex/Puzzle.ML src/HOLCF/IMP/Denotational.ML src/ZF/OrderType.ML src/ZF/ex/Acc.ML src/ZF/ex/ListN.ML src/ZF/ex/PropLog.ML