2006-04-09 wenzelm [Sun, 09 Apr 2006 18:51:13 +0200] rev 19380
tuned syntax/abbreviations;
src/FOL/IFOL.thy src/HOL/Algebra/Coset.thy src/HOL/Hyperreal/HyperDef.thy src/HOL/Hyperreal/HyperNat.thy src/HOL/Integ/NatBin.thy src/HOL/Integ/Numeral.thy src/HOL/Integ/Parity.thy src/HOL/Lambda/Eta.thy src/HOL/Lambda/Lambda.thy src/HOL/Lambda/Type.thy src/HOL/Lambda/WeakNorm.thy src/HOL/Library/Permutation.thy src/HOL/Library/SetsAndFunctions.thy src/HOL/W0/W0.thy src/HOL/ex/Higher_Order_Logic.thy

2006-04-09 wenzelm [Sun, 09 Apr 2006 18:51:11 +0200] rev 19379
unfold(ed): not necessrily meta equations;
doc-src/IsarRef/generic.tex

2006-04-09 nipkow [Sun, 09 Apr 2006 14:47:24 +0200] rev 19378
Made "empty" an abbreviation.
src/HOL/Map.thy

2006-04-09 nipkow [Sun, 09 Apr 2006 14:31:37 +0200] rev 19377
*** empty log message ***
NEWS

2006-04-09 nipkow [Sun, 09 Apr 2006 14:20:23 +0200] rev 19376
Removed old set interval syntax.
src/HOL/SetInterval.thy

2006-04-08 wenzelm [Sat, 08 Apr 2006 22:51:35 +0200] rev 19375
pretty_term: late externing of consts (support authentic syntax);
src/Pure/Syntax/syntax.ML

2006-04-08 wenzelm [Sat, 08 Apr 2006 22:51:33 +0200] rev 19374
pretty: late externing of consts (support authentic syntax);
src/Pure/Syntax/printer.ML

2006-04-08 wenzelm [Sat, 08 Apr 2006 22:51:31 +0200] rev 19373
removed fix_mixfix;
added const_mixfix, mixfix_const;
src/Pure/Syntax/mixfix.ML

2006-04-08 wenzelm [Sat, 08 Apr 2006 22:51:30 +0200] rev 19372
abbreviation(_i): do not expand abbreviations, do not use derived_def;
src/Pure/Isar/specification.ML

2006-04-08 wenzelm [Sat, 08 Apr 2006 22:51:28 +0200] rev 19371
add_abbrevs(_i): support print mode;
pretty_term': expand abbreviations only for well-typed terms;
added expand_abbrevs;
tuned;
src/Pure/Isar/proof_context.ML