2009-01-02 wenzelm [Fri, 02 Jan 2009 15:44:32 +0100] rev 29307
added id;
tuned;
src/Pure/General/position.ML

2009-01-02 wenzelm [Fri, 02 Jan 2009 11:31:40 +0100] rev 29306
MetaSimplifier.SIMPLIFIER;
src/ZF/Tools/inductive_package.ML

2009-01-02 wenzelm [Fri, 02 Jan 2009 11:31:07 +0100] rev 29305
fixed assumption proof;
src/FOLP/IFOLP.thy

2009-01-02 wenzelm [Fri, 02 Jan 2009 00:21:59 +0100] rev 29304
tuned header and description of boot files;
src/HOL/Complex_Main.thy src/HOL/Main.thy src/HOL/Plain.thy src/HOL/ROOT.ML src/HOL/main.ML src/HOL/plain.ML

2009-01-01 wenzelm [Thu, 01 Jan 2009 23:31:59 +0100] rev 29303
merged;

2009-01-01 wenzelm [Thu, 01 Jan 2009 23:31:49 +0100] rev 29302
normalized some ML type/val aliases;
src/HOL/Statespace/distinct_tree_prover.ML src/HOL/Statespace/state_fun.ML src/HOL/Tools/TFL/rules.ML src/HOL/Tools/arith_data.ML src/HOL/Tools/datatype_codegen.ML src/HOL/Tools/function_package/fundef_lib.ML src/Pure/Isar/code.ML src/Pure/Isar/find_theorems.ML src/ZF/Tools/inductive_package.ML

2009-01-01 wenzelm [Thu, 01 Jan 2009 22:57:42 +0100] rev 29301
assumption/close: discontinued implicit prems;
src/Pure/Isar/method.ML

2009-01-01 wenzelm [Thu, 01 Jan 2009 22:37:34 +0100] rev 29300
avoid implicit use of prems;
src/HOL/Nominal/Examples/SOS.thy

2009-01-01 wenzelm [Thu, 01 Jan 2009 22:20:29 +0100] rev 29299
updated generated files;
doc-src/IsarOverview/Isar/document/Logic.tex

2009-01-01 wenzelm [Thu, 01 Jan 2009 22:20:08 +0100] rev 29298
eliminated implicit use of prems;
unified fact names: a, b, ab;
doc-src/IsarOverview/Isar/Logic.thy