2012-05-24 kuncar [Thu, 24 May 2012 15:03:06 +0200] rev 47984
merged

2012-05-24 kuncar [Thu, 24 May 2012 14:20:25 +0200] rev 47983
drop the feature that more than one quotient type can be defined by quotient_type -> it causes problems
src/HOL/Tools/Quotient/quotient_type.ML

2012-05-24 kuncar [Thu, 24 May 2012 14:20:23 +0200] rev 47982
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
src/HOL/Library/Quotient_List.thy src/HOL/Library/Quotient_Option.thy src/HOL/Library/Quotient_Product.thy src/HOL/Library/Quotient_Set.thy src/HOL/Library/Quotient_Sum.thy src/HOL/Lifting.thy src/HOL/Tools/Lifting/lifting_def.ML src/HOL/Tools/Lifting/lifting_info.ML src/HOL/Tools/Lifting/lifting_setup.ML

2012-05-24 blanchet [Thu, 24 May 2012 15:01:29 +0200] rev 47981
gracefully handle definition-looking premises
src/HOL/Tools/ATP/atp_problem_generate.ML src/HOL/Tools/ATP/atp_systems.ML

2012-05-24 wenzelm [Thu, 24 May 2012 15:33:45 +0200] rev 47980
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
src/Pure/General/linear_set.ML src/Pure/General/table.ML src/Pure/IsaMakefile src/Pure/ML-Systems/compiler_polyml-5.3.ML src/Pure/ML-Systems/compiler_polyml.ML src/Pure/ML-Systems/polyml.ML src/Pure/ML-Systems/polyml_common.ML src/Pure/ML/install_pp_polyml-5.3.ML src/Pure/ML/install_pp_polyml.ML src/Pure/ML/ml_compiler_polyml-5.3.ML src/Pure/ML/ml_compiler_polyml.ML src/Pure/ROOT.ML src/Pure/pure_setup.ML

2012-05-24 wenzelm [Thu, 24 May 2012 15:01:17 +0200] rev 47979
discontinued support for Poly/ML 5.2.1;
Admin/CHECKLIST Admin/isatest/settings/at-poly NEWS src/Pure/IsaMakefile src/Pure/ML-Systems/compiler_polyml-5.2.ML src/Pure/ML-Systems/multithreading_polyml.ML src/Pure/ML-Systems/polyml-5.2.1.ML src/Pure/ML-Systems/pp_polyml.ML src/Pure/ML/install_pp_polyml.ML src/Pure/ROOT.ML src/Pure/pure_setup.ML

2012-05-24 wenzelm [Thu, 24 May 2012 14:46:14 +0200] rev 47978
less specific sample usage;
doc-src/System/Thy/Presentation.thy doc-src/System/Thy/document/Presentation.tex

2012-05-24 wenzelm [Thu, 24 May 2012 13:56:21 +0200] rev 47977
some post-release notes;
Admin/CHECKLIST

2012-05-23 blanchet [Wed, 23 May 2012 21:19:48 +0200] rev 47976
tuned names
src/HOL/Tools/ATP/atp_problem.ML src/HOL/Tools/ATP/atp_systems.ML src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

2012-05-23 blanchet [Wed, 23 May 2012 21:19:48 +0200] rev 47975
order LEO-II/Satallax definitions so that they build on each other (cf. Satallax's THF policy)
src/HOL/Tools/ATP/atp_problem_generate.ML