2009-10-25 chaieb [Sun, 25 Oct 2009 08:57:36 +0100] rev 33154
Multivariate polynomials library over fields
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy

2009-10-25 chaieb [Sun, 25 Oct 2009 08:57:36 +0100] rev 33153
A theory of polynomials based on lists
src/HOL/Decision_Procs/Polynomial_List.thy

2009-10-25 chaieb [Sun, 25 Oct 2009 08:57:35 +0100] rev 33152
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
src/HOL/Decision_Procs/Decision_Procs.thy src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy

2009-10-25 wenzelm [Sun, 25 Oct 2009 00:10:25 +0200] rev 33151
merged

2009-10-24 bulwahn [Sat, 24 Oct 2009 20:27:26 +0200] rev 33150
further changes due to the previous merge in the predicate compiler
src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML src/HOL/Tools/Predicate_Compile/pred_compile_data.ML src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML src/HOL/ex/Predicate_Compile_Alternative_Defs.thy

2009-10-24 wenzelm [Sat, 24 Oct 2009 23:57:42 +0200] rev 33149
merge -- imported from bulwahn d759e2728188;
src/HOL/Tools/Predicate_Compile/pred_compile_data.ML src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML src/HOL/Tools/Predicate_Compile/predicate_compile.ML src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

2009-10-24 bulwahn [Sat, 24 Oct 2009 16:55:43 +0200] rev 33148
removed tuple functions from the predicate compiler
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

2009-10-24 bulwahn [Sat, 24 Oct 2009 16:55:43 +0200] rev 33147
improving the compilation with higher-order arguments in the predicate compiler
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML src/HOL/ex/Predicate_Compile_ex.thy

2009-10-24 bulwahn [Sat, 24 Oct 2009 16:55:43 +0200] rev 33146
now the predicate compilere handles the predicate without introduction rules better as before
src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML src/HOL/Tools/Predicate_Compile/predicate_compile.ML src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML src/HOL/ex/Predicate_Compile_ex.thy

2009-10-24 bulwahn [Sat, 24 Oct 2009 16:55:43 +0200] rev 33145
removed dead code; added examples
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML src/HOL/ex/Predicate_Compile_ex.thy