2000-03-13 wenzelm [Mon, 13 Mar 2000 13:17:52 +0100] rev 8429
added Not;
src/HOL/hologic.ML

2000-03-13 wenzelm [Mon, 13 Mar 2000 13:16:57 +0100] rev 8428
adapted to new PureThy.add_thms etc.;
src/HOL/Tools/record_package.ML src/HOL/Tools/typedef_package.ML src/Pure/Isar/isar_thy.ML

2000-03-13 wenzelm [Mon, 13 Mar 2000 13:16:43 +0100] rev 8427
tuned;
src/Pure/Isar/rule_cases.ML

2000-03-13 wenzelm [Mon, 13 Mar 2000 13:16:26 +0100] rev 8426
cases: preserve order;
src/Pure/Isar/proof_context.ML

2000-03-13 nipkow [Mon, 13 Mar 2000 13:13:46 +0100] rev 8425
*** empty log message ***
NEWS

2000-03-13 nipkow [Mon, 13 Mar 2000 13:11:16 +0100] rev 8424
exhaust -> cases
doc-src/HOL/HOL.tex

2000-03-13 nipkow [Mon, 13 Mar 2000 12:51:10 +0100] rev 8423
exhaust_tac -> cases_tac
src/HOL/Arith.ML src/HOL/BCV/DFAimpl.ML src/HOL/BCV/Machine.ML src/HOL/BCV/Orders.ML src/HOL/BCV/Orders0.ML src/HOL/BCV/SemiLattice.ML src/HOL/BCV/Types0.ML src/HOL/Finite.ML src/HOL/Hoare/Examples.ML src/HOL/IMP/Transition.ML src/HOL/IOA/IOA.ML src/HOL/Induct/LList.ML src/HOL/Integ/Int.ML src/HOL/Integ/NatBin.ML src/HOL/Lambda/Eta.ML src/HOL/Lambda/InductTermi.ML src/HOL/Lambda/ListBeta.ML src/HOL/Lambda/ListOrder.ML src/HOL/Lex/MaxPrefix.ML src/HOL/Lex/NAe.ML src/HOL/Lex/Prefix.ML src/HOL/Lex/RegExp2NA.ML src/HOL/Lex/RegExp2NAe.ML src/HOL/Lex/RegSet_of_nat_DA.ML src/HOL/List.ML src/HOL/MicroJava/BV/BVSpecTypeSafe.ML src/HOL/MicroJava/BV/Convert.ML src/HOL/MicroJava/BV/Correct.ML src/HOL/MicroJava/BV/LBVComplete.ML src/HOL/MicroJava/BV/LBVCorrect.ML src/HOL/MicroJava/BV/LBVSpec.ML src/HOL/MicroJava/J/JBasis.ML src/HOL/MicroJava/J/JTypeSafe.ML src/HOL/MicroJava/J/Type.ML src/HOL/Nat.ML src/HOL/Option.ML src/HOL/Power.ML src/HOL/Real/RealPow.ML src/HOL/RelPow.ML src/HOL/TLA/Inc/Inc.ML src/HOL/TLA/Memory/Memory.ML src/HOL/UNITY/GenPrefix.ML src/HOL/UNITY/Lift_prog.ML src/HOL/UNITY/TimerArray.ML src/HOL/UNITY/Token.ML src/HOL/ex/BinEx.ML src/HOL/ex/Factorization.ML src/HOL/ex/Primrec.ML src/HOL/ex/Puzzle.ML

2000-03-13 paulson [Mon, 13 Mar 2000 12:42:41 +0100] rev 8422
renamed "f" to "le" and "mset" to "multiset"
src/HOL/ex/InSort.ML src/HOL/ex/InSort.thy

2000-03-13 paulson [Mon, 13 Mar 2000 12:42:05 +0100] rev 8421
fixed the goal statement of sorted_qsort
src/HOL/ex/Qsort.ML

2000-03-13 wenzelm [Mon, 13 Mar 2000 12:25:52 +0100] rev 8420
adapted to new PureThy.add_thms etc.;
src/Pure/Thy/thy_parse.ML src/Pure/axclass.ML