2007-10-20 wenzelm [Sat, 20 Oct 2007 18:54:35 +0200] rev 25122
moved internalM to PrintMode.internal;
PrintMode.input;
src/Pure/Syntax/syntax.ML

2007-10-20 wenzelm [Sat, 20 Oct 2007 18:54:34 +0200] rev 25121
tuned abbrev interface;
PrintMode.internal;
src/Pure/Isar/theory_target.ML

2007-10-20 wenzelm [Sat, 20 Oct 2007 18:54:33 +0200] rev 25120
tuned abbrev interface;
src/Pure/Isar/local_theory.ML

2007-10-20 wenzelm [Sat, 20 Oct 2007 18:54:33 +0200] rev 25119
added fixed_abbrev;
src/Pure/Isar/local_defs.ML

2007-10-20 wenzelm [Sat, 20 Oct 2007 18:54:31 +0200] rev 25118
added input/internal, which are never active in print_mode_value;
src/Pure/General/print_mode.ML

2007-10-20 wenzelm [Sat, 20 Oct 2007 18:54:30 +0200] rev 25117
no_variables: tuned error msg;
src/Pure/sign.ML

2007-10-20 wenzelm [Sat, 20 Oct 2007 18:54:29 +0200] rev 25116
PrintMode.internal;
src/Pure/consts.ML

2007-10-20 wenzelm [Sat, 20 Oct 2007 18:54:28 +0200] rev 25115
tuned;
etc/settings

2007-10-20 wenzelm [Sat, 20 Oct 2007 18:54:28 +0200] rev 25114
add_inductive: more careful handling of abbrevs -- do not expand prematurely;
src/HOL/Tools/inductive_package.ML

2007-10-20 wenzelm [Sat, 20 Oct 2007 15:46:04 +0200] rev 25113
fixed proof: neq0_conv;
src/HOLCF/IOA/NTP/Impl.thy