1998-03-09 wenzelm [Mon, 09 Mar 1998 16:09:06 +0100] rev 4693
adapted to baroque chars;
src/Pure/logic.ML src/Pure/tactic.ML

1998-03-09 wenzelm [Mon, 09 Mar 1998 16:08:37 +0100] rev 4692
added merge_alists;
moced is_letter etc. to Syntax/symbol.ML;
src/Pure/library.ML

1998-03-09 wenzelm [Mon, 09 Mar 1998 16:08:06 +0100] rev 4691
Syntax.indexname;
src/Pure/drule.ML

1998-03-09 wenzelm [Mon, 09 Mar 1998 16:07:22 +0100] rev 4690
tuned comment;
src/Pure/ROOT.ML

1998-03-09 wenzelm [Mon, 09 Mar 1998 16:07:03 +0100] rev 4689
tuned;
src/Pure/README src/Pure/Syntax/README

1998-03-09 wenzelm [Mon, 09 Mar 1998 16:06:46 +0100] rev 4688
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
added Pure/Syntax/scan.ML;
src/Pure/IsaMakefile

1998-03-09 wenzelm [Mon, 09 Mar 1998 16:05:34 +0100] rev 4687
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
Admin/fixencoding src/Pure/Syntax/symbol.ML src/Pure/Syntax/symbol_font.ML

1998-03-07 nipkow [Sat, 07 Mar 1998 16:29:29 +0100] rev 4686
Removed `addsplits [expand_if]'
src/HOL/Arith.ML src/HOL/Auth/Event.ML src/HOL/Auth/Message.ML src/HOL/Auth/NS_Public.ML src/HOL/Auth/NS_Public_Bad.ML src/HOL/Auth/Public.ML src/HOL/Auth/Shared.ML src/HOL/Auth/TLS.ML src/HOL/Auth/Yahalom2.ML src/HOL/Divides.ML src/HOL/Finite.ML src/HOL/IMP/Hoare.ML src/HOL/Induct/Com.ML src/HOL/Induct/LFilter.ML src/HOL/Induct/Mutil.ML src/HOL/Induct/Perm.ML src/HOL/Induct/PropLog.ML src/HOL/Induct/SList.ML src/HOL/Integ/Bin.ML src/HOL/Lambda/Eta.ML src/HOL/Lambda/Lambda.ML src/HOL/Lex/AutoChopper.ML src/HOL/Lex/Regset_of_auto.ML src/HOL/List.ML src/HOL/Map.ML src/HOL/MiniML/Generalize.ML src/HOL/MiniML/Instance.ML src/HOL/MiniML/MiniML.ML src/HOL/MiniML/Type.ML src/HOL/MiniML/W.ML src/HOL/Nat.ML src/HOL/NatDef.ML src/HOL/Ord.ML src/HOL/Set.ML src/HOL/Subst/Subst.ML src/HOL/Subst/Unifier.ML src/HOL/Subst/Unify.ML src/HOL/W0/I.ML src/HOL/W0/Type.ML src/HOL/W0/W.ML src/HOL/WF.ML src/HOL/equalities.ML src/HOL/ex/Fib.ML src/HOL/ex/InSort.ML src/HOL/ex/Primes.ML src/HOL/ex/Qsort.ML src/HOL/ex/Recdef.ML src/HOL/ex/Sorting.ML src/HOL/ex/set.ML

1998-03-06 wenzelm [Fri, 06 Mar 1998 18:25:28 +0100] rev 4685
added clasimp.ML;
src/FOL/IsaMakefile

1998-03-06 nipkow [Fri, 06 Mar 1998 16:05:04 +0100] rev 4684
Removed superfluous `op'
src/Pure/thm.ML