1998-09-24 oheimb [Thu, 24 Sep 1998 17:16:06 +0200] rev 5552
simplified CLASIMP_DATA
renamed mk_meta_eq to mk_eq, meta_eq to mk_meta_eq
src/HOL/simpdata.ML

1998-09-24 paulson [Thu, 24 Sep 1998 17:07:24 +0200] rev 5551
renamed some axioms; some new theorems
src/HOL/Integ/Bin.ML

1998-09-24 oheimb [Thu, 24 Sep 1998 16:53:14 +0200] rev 5550
introduced addSE2, addSD2, addE2, and addD2
reflected changes to addbefore, addSbefore
described setup of clasimp.ML
introduced clarsimp_tac and Clarsimp_tac
doc-src/Ref/classical.tex

1998-09-24 oheimb [Thu, 24 Sep 1998 16:53:00 +0200] rev 5549
improved description of looper and splitter
reflected changes of mk_meta_eq, ...
doc-src/Ref/simplifier.tex

1998-09-24 oheimb [Thu, 24 Sep 1998 15:36:16 +0200] rev 5548
workaround for litte bug in our ln command
doc-src/Intro/Makefile doc-src/Logics/Makefile doc-src/Ref/Makefile doc-src/System/Makefile doc-src/Tutorial/Makefile

1998-09-24 paulson [Thu, 24 Sep 1998 15:23:47 +0200] rev 5547
Function nat_of now maps negative integers to zero, not their absolute value
src/HOL/Integ/Integ.ML src/HOL/Integ/Integ.thy

1998-09-24 paulson [Thu, 24 Sep 1998 15:21:30 +0200] rev 5546
renamed some axioms
src/HOL/Integ/Bin.thy

1998-09-24 paulson [Thu, 24 Sep 1998 15:20:29 +0200] rev 5545
added correctness proofs for arithmetic
src/HOL/ex/BinEx.ML src/HOL/ex/BinEx.thy

1998-09-24 paulson [Thu, 24 Sep 1998 15:20:03 +0200] rev 5544
new induction rule for integers
src/HOL/UNITY/SubstAx.ML

1998-09-24 oheimb [Thu, 24 Sep 1998 11:00:07 +0200] rev 5543
fixed calls of ln, rm
doc-src/Ref/Makefile