2010-02-23 blanchet [Tue, 23 Feb 2010 14:11:36 +0100] rev 35331
document Quickcheck's "no_assms" option
doc-src/IsarRef/Thy/HOL_Specific.thy doc-src/Nitpick/nitpick.tex

2010-02-24 haftmann [Wed, 24 Feb 2010 11:21:37 +0100] rev 35330
tuned comment
src/HOL/Algebra/abstract/Ring2.thy

2010-02-23 hoelzl [Tue, 23 Feb 2010 17:55:00 +0100] rev 35329
merged
src/HOL/IsaMakefile

2010-02-23 hoelzl [Tue, 23 Feb 2010 17:33:03 +0100] rev 35328
Moved old Integration to examples.
src/HOL/Integration.thy src/HOL/IsaMakefile src/HOL/ex/Gauge_Integration.thy src/HOL/ex/ROOT.ML

2010-02-23 bulwahn [Tue, 23 Feb 2010 16:58:21 +0100] rev 35327
merged
src/HOL/Hoare/HoareAbort.thy src/HOL/W0/README.html src/HOL/W0/ROOT.ML src/HOL/W0/W0.thy src/HOL/W0/document/root.tex

2010-02-23 bulwahn [Tue, 23 Feb 2010 14:00:36 +0100] rev 35326
merged

2010-02-23 bulwahn [Tue, 23 Feb 2010 13:57:51 +0100] rev 35325
adding ROOT.ML to HOL-Mutabelle session; uncommenting HOL.induct constants in Mutabelle session
src/HOL/Mutabelle/ROOT.ML src/HOL/Mutabelle/mutabelle_extra.ML

2010-02-23 bulwahn [Tue, 23 Feb 2010 13:36:15 +0100] rev 35324
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
src/HOL/Mutabelle/mutabelle_extra.ML src/HOL/Tools/Datatype/datatype_prop.ML src/HOL/Tools/Function/function.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_core.ML src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML src/HOL/ex/Predicate_Compile_Alternative_Defs.thy src/HOL/ex/Predicate_Compile_Quickcheck.thy src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy src/HOL/ex/Predicate_Compile_ex.thy src/Tools/quickcheck.ML

2010-02-23 boehmes [Tue, 23 Feb 2010 15:20:19 +0100] rev 35323
separated narrowing timeouts for intermediate and final steps
src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy src/HOL/Boogie/Tools/boogie_commands.ML

2010-02-23 haftmann [Tue, 23 Feb 2010 14:13:14 +0100] rev 35322
merged
src/HOL/Hoare/HoareAbort.thy src/HOL/W0/README.html src/HOL/W0/ROOT.ML src/HOL/W0/W0.thy src/HOL/W0/document/root.tex