2000-06-16 paulson [Fri, 16 Jun 2000 13:21:17 +0200] rev 9079
some missing simprules for integer linear arithmetic
src/HOL/Integ/IntArith.ML

2000-06-16 paulson [Fri, 16 Jun 2000 13:19:15 +0200] rev 9078
tidied for new card_seteq
src/HOL/IMPP/Hoare.ML

2000-06-16 paulson [Fri, 16 Jun 2000 13:18:55 +0200] rev 9077
subset_empty is no longer a simprule
src/HOL/equalities.ML

2000-06-16 paulson [Fri, 16 Jun 2000 13:16:07 +0200] rev 9076
renamed psubset_card -> psubset_card_mono
src/HOL/WF_Rel.ML

2000-06-16 paulson [Fri, 16 Jun 2000 13:15:40 +0200] rev 9075
Finally "AddEs [equalityE]" is IN and "AddDs [equals0D, sym RS equals0D]" is OUT
src/HOL/Set.ML

2000-06-16 paulson [Fri, 16 Jun 2000 13:15:04 +0200] rev 9074
inserted some "addsimps [subset_empty]"; also tidied (a lot)
src/HOL/Finite.ML

2000-06-16 paulson [Fri, 16 Jun 2000 13:13:55 +0200] rev 9073
tracing flag for arith_tac
src/HOL/Arith.ML src/Provers/Arith/fast_lin_arith.ML

2000-06-15 berghofe [Thu, 15 Jun 2000 16:02:12 +0200] rev 9072
Now also proves monotonicity when in quick_and_dirty mode.
src/HOL/Tools/inductive_package.ML

2000-06-14 paulson [Wed, 14 Jun 2000 18:24:41 +0200] rev 9071
tidied
src/HOL/Real/Hyperreal/HyperDef.ML

2000-06-14 paulson [Wed, 14 Jun 2000 18:23:51 +0200] rev 9070
full_rename_numerals -> rename_numerals; tidied
src/HOL/Real/RealPow.ML