src/HOL/Multivariate_Analysis/Integration.thy
Thu, 01 Jul 2010 11:48:42 +0200 hoelzl Add theory for indicator function.
Mon, 21 Jun 2010 19:33:51 +0200 hoelzl Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
Wed, 12 May 2010 23:54:04 +0200 boehmes layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
Tue, 11 May 2010 19:21:05 +0200 hoelzl Removed usage of normalizating locales.
Sun, 09 May 2010 22:51:11 -0700 huffman avoid using real-specific versions of generic lemmas
Fri, 07 May 2010 09:59:24 +0200 haftmann prefix normalizing replaces class_semiring
Wed, 28 Apr 2010 22:20:59 -0700 huffman remove redundant lemma vector_dist_norm
Mon, 26 Apr 2010 09:45:22 -0700 huffman merged
Mon, 26 Apr 2010 09:21:25 -0700 huffman fix lots of looping simp calls and other warnings
Sun, 25 Apr 2010 16:23:40 -0700 huffman generalize type of continuous_on
Mon, 26 Apr 2010 11:34:19 +0200 haftmann dropped group_simps, ring_simps, field_eq_simps
Sat, 24 Apr 2010 13:31:52 -0700 huffman document generation for Multivariate_Analysis
Fri, 23 Apr 2010 23:33:48 +0200 wenzelm eliminated spurious schematic statements;
Wed, 21 Apr 2010 10:44:44 +0200 hoelzl Only use provided SMT-certificates in HOL-Multivariate_Analysis.
Tue, 20 Apr 2010 14:07:52 +0200 himmelma Translated remaining theorems about integration from HOL light.
Wed, 07 Apr 2010 19:48:58 +0200 boehmes renamed "smt_record" to "smt_fixed" (somewhat more expressive) and inverted its semantics
Wed, 24 Mar 2010 14:03:52 +0100 boehmes inhibit invokation of external SMT solver
Tue, 09 Mar 2010 15:42:23 +0100 himmelma reset smt_certificates
Tue, 09 Mar 2010 15:39:26 +0100 himmelma added lemmas
Tue, 02 Mar 2010 09:57:49 +0100 himmelma the ordering on real^1 is linear
Mon, 22 Feb 2010 20:41:49 +0100 hoelzl Replaced Integration by Multivariate-Analysis/Real_Integration
Wed, 17 Feb 2010 18:33:45 +0100 himmelma Added integration to Multivariate-Analysis (upto FTC)
less more (0) tip