2011-04-19 wenzelm [Tue, 19 Apr 2011 23:57:28 +0200] rev 42411
eliminated Codegen.mode in favour of explicit argument;
src/HOL/HOL.thy src/HOL/Int.thy src/HOL/List.thy src/HOL/Product_Type.thy src/HOL/String.thy src/HOL/Tools/Datatype/datatype_codegen.ML src/HOL/Tools/inductive_codegen.ML src/HOL/Tools/recfun_codegen.ML src/Pure/codegen.ML

2011-04-19 wenzelm [Tue, 19 Apr 2011 22:32:49 +0200] rev 42410
less bulky "_position", for improved readability of parse trees;
src/Pure/Syntax/syntax_phases.ML src/Pure/pure_thy.ML

2011-04-19 wenzelm [Tue, 19 Apr 2011 22:08:42 +0200] rev 42409
added more elementary Skip_Proof.make_thm_cterm;
src/Pure/Isar/skip_proof.ML

2011-04-19 wenzelm [Tue, 19 Apr 2011 21:55:42 +0200] rev 42408
explicit markup for loose bounds;
src/Pure/Syntax/syntax.ML src/Pure/Syntax/syntax_phases.ML

2011-04-19 wenzelm [Tue, 19 Apr 2011 21:33:56 +0200] rev 42407
prefer internal types, via Simple_Syntax.read_typ;
src/Pure/Proof/extraction.ML

2011-04-19 wenzelm [Tue, 19 Apr 2011 21:19:14 +0200] rev 42406
eliminated obsolete Proof_Syntax.strip_sorts_consttypes;
src/Pure/Proof/extraction.ML src/Pure/Proof/proof_syntax.ML

2011-04-19 wenzelm [Tue, 19 Apr 2011 20:47:02 +0200] rev 42405
split Type_Infer into early and late part, after Proof_Context;
added Type_Infer_Context.const_sorts option, which allows NBE to use regular Syntax.check_term;
src/Pure/IsaMakefile src/Pure/Isar/proof_context.ML src/Pure/ROOT.ML src/Pure/type_infer.ML src/Pure/type_infer_context.ML src/Tools/nbe.ML src/Tools/subtyping.ML

2011-04-19 wenzelm [Tue, 19 Apr 2011 16:13:04 +0200] rev 42404
minor tuning and modernization;
src/Pure/Isar/overloading.ML

2011-04-19 wenzelm [Tue, 19 Apr 2011 15:58:05 +0200] rev 42403
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
NEWS src/Pure/Syntax/syntax.ML src/Pure/library.ML

2011-04-19 wenzelm [Tue, 19 Apr 2011 14:57:09 +0200] rev 42402
simplified check/uncheck interfaces: result comparison is hardwired by default;
tuned;
src/HOL/Tools/code_evaluation.ML src/Pure/Isar/class.ML src/Pure/Isar/class_declaration.ML src/Pure/Isar/overloading.ML src/Pure/Isar/proof_context.ML src/Pure/Syntax/syntax.ML src/Tools/adhoc_overloading.ML src/Tools/subtyping.ML