2012-05-24 wenzelm [Thu, 24 May 2012 17:25:53 +0200] rev 47988
tuned proofs;
src/HOL/Hilbert_Choice.thy src/HOL/Nat.thy src/HOL/Nitpick.thy src/HOL/Product_Type.thy src/HOL/Set_Interval.thy

2012-05-24 wenzelm [Thu, 24 May 2012 17:05:30 +0200] rev 47987
reparse descendants after update of imports, e.g. required for 'primrec' (line 17 of "src/HOL/Power.thy");
src/Pure/Thy/thy_syntax.scala

2012-05-24 wenzelm [Thu, 24 May 2012 15:54:38 +0200] rev 47986
merged
src/Pure/ML-Systems/compiler_polyml-5.2.ML src/Pure/ML-Systems/compiler_polyml-5.3.ML src/Pure/ML-Systems/polyml-5.2.1.ML src/Pure/ML-Systems/polyml_common.ML src/Pure/ML-Systems/pp_polyml.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

2012-05-24 blanchet [Thu, 24 May 2012 15:11:53 +0200] rev 47985
update Satallax setup based on evaluation
src/HOL/Tools/ATP/atp_systems.ML

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