2010-02-27 wenzelm [Sat, 27 Feb 2010 22:52:06 +0100] rev 35406
further standard instances of functor Graph;
src/Pure/term_ord.ML

2010-02-27 wenzelm [Sat, 27 Feb 2010 22:41:22 +0100] rev 35405
code simplification by inlining;
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML src/Pure/General/graph.ML

2010-02-27 wenzelm [Sat, 27 Feb 2010 21:56:55 +0100] rev 35404
just one copy of structure Term_Graph (in Pure);
src/HOL/Tools/Function/termination.ML src/HOL/Tools/Predicate_Compile/predicate_compile.ML src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML src/Pure/term_ord.ML

2010-02-27 wenzelm [Sat, 27 Feb 2010 21:56:05 +0100] rev 35403
modernized structure Int_Graph;
src/HOL/Tools/Function/context_tree.ML src/Pure/General/graph.ML

2010-02-27 wenzelm [Sat, 27 Feb 2010 20:57:08 +0100] rev 35402
clarified @{const_name} vs. @{const_abbrev};
src/HOL/Library/Multiset.thy src/HOL/Nominal/nominal_datatype.ML src/HOL/Rat.thy src/HOL/Tools/Datatype/datatype.ML src/HOL/Tools/Function/function_lib.ML src/HOL/Tools/Function/lexicographic_order.ML src/HOL/Tools/Function/termination.ML src/HOL/Tools/Nitpick/nitpick_model.ML src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML src/HOL/Tools/Quotient/quotient_term.ML src/HOL/Tools/inductive_realizer.ML

2010-02-27 wenzelm [Sat, 27 Feb 2010 20:56:03 +0100] rev 35401
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
tuned;
NEWS src/Pure/ML/ml_antiquote.ML

2010-02-27 wenzelm [Sat, 27 Feb 2010 20:55:18 +0100] rev 35400
type/const name: explicitly allow abbreviations as well;
src/Tools/induct.ML

2010-02-27 wenzelm [Sat, 27 Feb 2010 20:51:51 +0100] rev 35399
clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
src/Pure/Isar/args.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/specification.ML src/Pure/Thy/thy_output.ML

2010-02-27 wenzelm [Sat, 27 Feb 2010 13:55:03 +0100] rev 35398
added at-poly-test, which is intended for performance tests of Poly/ML itself;
Admin/isatest/isatest-makedist Admin/isatest/settings/at-poly-test

2010-02-27 wenzelm [Sat, 27 Feb 2010 13:32:55 +0100] rev 35397
more precise syntax antiquotations;
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy