2000-09-11 wenzelm [Mon, 11 Sep 2000 17:37:09 +0200] rev 9916
define \isabellecontext;
src/Pure/Thy/latex.ML

2000-09-11 wenzelm [Mon, 11 Sep 2000 17:35:50 +0200] rev 9915
added THIS;
configure

2000-09-11 wenzelm [Mon, 11 Sep 2000 17:35:17 +0200] rev 9914
case args: align_right;
src/HOL/Tools/induct_method.ML

2000-09-11 wenzelm [Mon, 11 Sep 2000 17:34:42 +0200] rev 9913
added \isabellecontext;
tuned;
lib/texinputs/isabelle.sty

2000-09-11 paulson [Mon, 11 Sep 2000 13:03:11 +0200] rev 9912
tidied
src/HOL/Divides.ML src/HOL/ex/Primes.thy

2000-09-08 wenzelm [Fri, 08 Sep 2000 12:13:21 +0200] rev 9911
*** empty log message ***
doc-src/TutorialI/Misc/document/simp.tex

2000-09-07 wenzelm [Thu, 07 Sep 2000 22:37:59 +0200] rev 9910
internalize error "insufficient syntax for prefix application";
src/Pure/Syntax/printer.ML

2000-09-07 wenzelm [Thu, 07 Sep 2000 21:21:07 +0200] rev 9909
tuned ML code (the_context, bind_thms(s));
src/ZF/Integ/Bin.ML src/ZF/Integ/EquivClass.ML src/ZF/Integ/Int.ML

2000-09-07 wenzelm [Thu, 07 Sep 2000 21:18:18 +0200] rev 9908
HOL: qed_spec_mp now also removes bounded ALL;
Isar: renamed some attributes;
NEWS

2000-09-07 wenzelm [Thu, 07 Sep 2000 21:12:49 +0200] rev 9907
tuned ML code (the_context, bind_thms(s));
src/ZF/AC.ML src/ZF/Arith.ML src/ZF/ArithSimp.ML src/ZF/Bool.ML src/ZF/Cardinal.ML src/ZF/CardinalArith.ML src/ZF/Cardinal_AC.ML src/ZF/Epsilon.ML src/ZF/Finite.ML src/ZF/Fixedpt.ML src/ZF/InfDatatype.ML src/ZF/Let.ML src/ZF/List.ML src/ZF/Nat.ML src/ZF/OrdQuant.ML src/ZF/OrderArith.ML src/ZF/OrderType.ML src/ZF/Ordinal.ML src/ZF/Perm.ML src/ZF/QPair.ML src/ZF/QUniv.ML src/ZF/Rel.ML src/ZF/Sum.ML src/ZF/Trancl.ML src/ZF/Univ.ML src/ZF/Update.ML src/ZF/WF.ML src/ZF/ZF.ML src/ZF/Zorn.ML src/ZF/equalities.ML src/ZF/func.ML src/ZF/mono.ML src/ZF/simpdata.ML src/ZF/subset.ML src/ZF/upair.ML src/ZF/upair.thy