2010-02-22 hoelzl [Mon, 22 Feb 2010 20:41:49 +0100] rev 35292
Replaced Integration by Multivariate-Analysis/Real_Integration
src/HOL/Complex_Main.thy src/HOL/Integration.thy src/HOL/IsaMakefile src/HOL/Multivariate_Analysis/Integration.cert src/HOL/Multivariate_Analysis/Integration.thy src/HOL/Multivariate_Analysis/Integration_MV.cert src/HOL/Multivariate_Analysis/Integration_MV.thy src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy src/HOL/Multivariate_Analysis/Real_Integration.thy src/HOL/SEQ.thy

2010-02-22 himmelma [Mon, 22 Feb 2010 20:08:10 +0100] rev 35291
Support for one-dimensional integration in Multivariate-Analysis
src/HOL/Multivariate_Analysis/Integration_MV.cert src/HOL/Multivariate_Analysis/Integration_MV.thy

2010-02-18 himmelma [Thu, 18 Feb 2010 22:11:19 +0100] rev 35290
Equivalence between DERIV and one-dimensional derivation in Multivariate-Analysis
src/HOL/Multivariate_Analysis/Derivative.thy

2010-02-22 huffman [Mon, 22 Feb 2010 11:19:15 -0800] rev 35289
merged
src/HOLCF/IOA/meta_theory/Seq.thy

2010-02-22 huffman [Mon, 22 Feb 2010 11:17:41 -0800] rev 35288
add mixfix field to type Domain_Library.cons
src/HOLCF/Tools/Domain/domain_axioms.ML src/HOLCF/Tools/Domain/domain_extender.ML src/HOLCF/Tools/Domain/domain_library.ML src/HOLCF/Tools/Domain/domain_theorems.ML

2010-02-22 huffman [Mon, 22 Feb 2010 09:43:36 -0800] rev 35287
remove unnecessary local
src/HOLCF/Tools/Domain/domain_theorems.ML

2010-02-21 huffman [Sun, 21 Feb 2010 08:59:39 -0800] rev 35286
update to use fixrec package
src/HOLCF/IOA/meta_theory/Seq.thy

2010-02-22 blanchet [Mon, 22 Feb 2010 19:31:18 +0100] rev 35285
merge

2010-02-22 blanchet [Mon, 22 Feb 2010 19:31:00 +0100] rev 35284
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
doc-src/Nitpick/nitpick.tex src/HOL/Main.thy src/HOL/Nitpick.thy src/HOL/Nitpick_Examples/Core_Nits.thy src/HOL/Nitpick_Examples/Datatype_Nits.thy src/HOL/Nitpick_Examples/Hotel_Nits.thy src/HOL/Nitpick_Examples/Manual_Nits.thy src/HOL/Nitpick_Examples/Mini_Nits.thy src/HOL/Nitpick_Examples/Pattern_Nits.thy src/HOL/Nitpick_Examples/Record_Nits.thy src/HOL/Nitpick_Examples/Refute_Nits.thy src/HOL/Nitpick_Examples/Special_Nits.thy src/HOL/Nitpick_Examples/Typedef_Nits.thy src/HOL/Tools/Nitpick/minipick.ML src/HOL/Tools/Nitpick/nitpick_hol.ML src/HOL/Tools/Nitpick/nitpick_peephole.ML src/HOL/Tools/Nitpick/nitpick_preproc.ML src/HOL/Tools/Nitpick/nitpick_tests.ML

2010-02-22 blanchet [Mon, 22 Feb 2010 14:36:10 +0100] rev 35283
filter out trivial definitions in Nitpick (e.g. "Topology.topo" from AFP)
src/HOL/Tools/Nitpick/nitpick_hol.ML