2000-01-05 wenzelm [Wed, 05 Jan 2000 11:45:01 +0100] rev 8094
ObtainFun;
prepare vars / asms / pats only once;
src/Pure/Isar/obtain.ML

2000-01-05 wenzelm [Wed, 05 Jan 2000 11:43:37 +0100] rev 8093
added thms_ctxt_args;
src/Pure/Isar/method.ML

2000-01-05 wenzelm [Wed, 05 Jan 2000 11:43:09 +0100] rev 8092
prepare patterns only once;
src/Pure/Isar/local_defs.ML

2000-01-05 wenzelm [Wed, 05 Jan 2000 11:42:02 +0100] rev 8091
ObtainFun;
src/Pure/Isar/ROOT.ML

2000-01-05 wenzelm [Wed, 05 Jan 2000 11:41:38 +0100] rev 8090
present chapter;
tuned proof markup commands;
moved obtain to obtain.ML;
src/Pure/Isar/isar_thy.ML

2000-01-05 wenzelm [Wed, 05 Jan 2000 11:40:13 +0100] rev 8089
removed pats;
src/Pure/Isar/args.ML

2000-01-05 wenzelm [Wed, 05 Jan 2000 11:38:48 +0100] rev 8088
chapter;
src/Pure/Thy/html.ML src/Pure/Thy/present.ML

2000-01-05 wenzelm [Wed, 05 Jan 2000 11:37:44 +0100] rev 8087
support for dummy variables (anyT, logicT);
improved error msg: meet *before* assign;
src/Pure/type_infer.ML

2000-01-05 wenzelm [Wed, 05 Jan 2000 11:35:18 +0100] rev 8086
TypeInfer.logicT;
src/Pure/drule.ML src/Pure/goals.ML

2000-01-04 oheimb [Tue, 04 Jan 2000 17:05:43 +0100] rev 8085
new arg type for max_spec etc.
src/HOL/MicroJava/J/JTypeSafe.ML src/HOL/MicroJava/J/WellType.ML src/HOL/MicroJava/J/WellType.thy