2011-08-17 wenzelm [Wed, 17 Aug 2011 16:46:58 +0200] rev 44240
improved default context for ML toplevel pretty-printing;
src/Pure/Isar/proof_display.ML

2011-08-17 wenzelm [Wed, 17 Aug 2011 16:30:38 +0200] rev 44239
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
src/HOL/Tools/Function/fun.ML src/HOL/Tools/Function/function.ML

2011-08-17 wenzelm [Wed, 17 Aug 2011 16:01:27 +0200] rev 44238
some convenience actions/shortcuts for control symbols;
src/Pure/General/symbol.scala src/Pure/Thy/html.scala src/Tools/jEdit/src/Isabelle.props src/Tools/jEdit/src/actions.xml src/Tools/jEdit/src/plugin.scala src/Tools/jEdit/src/token_markup.scala

2011-08-17 wenzelm [Wed, 17 Aug 2011 15:14:48 +0200] rev 44237
export Function_Fun.fun_config for user convenience;
src/HOL/Tools/Function/fun.ML

2011-08-17 wenzelm [Wed, 17 Aug 2011 13:14:20 +0200] rev 44236
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
src/HOL/IsaMakefile src/HOL/Library/Library.thy src/HOL/Library/Nested_Environment.thy src/HOL/Unix/Nested_Environment.thy src/HOL/Unix/Unix.thy

2011-08-17 blanchet [Wed, 17 Aug 2011 10:03:58 +0200] rev 44235
distinguish THF syntax with and without choice (Satallax vs. LEO-II)
src/HOL/Tools/ATP/atp_problem.ML src/HOL/Tools/ATP/atp_systems.ML src/HOL/Tools/ATP/atp_translate.ML

2011-08-16 huffman [Tue, 16 Aug 2011 15:02:20 -0700] rev 44234
merged

2011-08-16 huffman [Tue, 16 Aug 2011 09:31:23 -0700] rev 44233
add simp rules for isCont
src/HOL/Deriv.thy src/HOL/Library/Inner_Product.thy src/HOL/Library/Product_Vector.thy src/HOL/Lim.thy src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy src/HOL/Multivariate_Analysis/Euclidean_Space.thy src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy

2011-08-16 wenzelm [Tue, 16 Aug 2011 23:39:58 +0200] rev 44232
updated keywords -- old codegen is no longer in Pure;
etc/isar-keywords-ZF.el

2011-08-16 wenzelm [Tue, 16 Aug 2011 23:39:30 +0200] rev 44231
include HOL-Library keywords for the sake of recdef;
Admin/update-keywords etc/isar-keywords.el