2000-05-24 wenzelm [Wed, 24 May 2000 19:09:50 +0200] rev 8966
added "done" proof;
src/Pure/Isar/isar_syn.ML src/Pure/Isar/isar_thy.ML src/Pure/Isar/method.ML

2000-05-24 wenzelm [Wed, 24 May 2000 19:09:36 +0200] rev 8965
proper token_translation for latex mode;
src/Pure/Thy/latex.ML src/Pure/pure.ML

2000-05-24 paulson [Wed, 24 May 2000 18:51:28 +0200] rev 8964
some lemmas about plus_ac0
src/HOL/HOL_lemmas.ML

2000-05-24 paulson [Wed, 24 May 2000 18:50:08 +0200] rev 8963
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
src/HOL/Finite.ML

2000-05-24 paulson [Wed, 24 May 2000 18:49:05 +0200] rev 8962
setsum is now overloaded on plus_ac0
src/HOL/Finite.thy

2000-05-24 paulson [Wed, 24 May 2000 18:48:22 +0200] rev 8961
installing plus_ac0 for nat
src/HOL/Divides.thy

2000-05-24 paulson [Wed, 24 May 2000 18:48:03 +0200] rev 8960
we must not require SetInterval this early
src/HOL/Fun.thy

2000-05-24 paulson [Wed, 24 May 2000 18:47:43 +0200] rev 8959
installing the plus_ac0 axclass
src/HOL/HOL.thy

2000-05-24 paulson [Wed, 24 May 2000 18:46:38 +0200] rev 8958
Adding SetInterval, deleting UNITY/LessThan
src/HOL/IsaMakefile

2000-05-24 paulson [Wed, 24 May 2000 18:46:06 +0200] rev 8957
added parent
src/HOL/SetInterval.thy