Thu, 17 Jun 2010 19:32:05 +0200 
haftmann 
replaced unreliable metis proof

file 
diff 
annotate

Sun, 09 May 2010 22:51:11 0700 
huffman 
avoid using realspecific versions of generic lemmas

file 
diff 
annotate

Tue, 04 May 2010 19:53:57 0700 
huffman 
generalize some lemmas to class t1_space

file 
diff 
annotate

Tue, 04 May 2010 19:23:59 0700 
huffman 
simplify definition of t1_space; generalize lemma closed_sing and related lemmas

file 
diff 
annotate

Tue, 04 May 2010 18:55:18 0700 
huffman 
generalize some lemmas

file 
diff 
annotate

Tue, 04 May 2010 10:06:05 0700 
huffman 
make (X > L) an abbreviation for (X > L) sequentially

file 
diff 
annotate

Tue, 04 May 2010 09:56:34 0700 
huffman 
adapt to removed premise on tendsto lemma (cf. 88f0125c3bd2)

file 
diff 
annotate

Mon, 03 May 2010 14:35:10 +0200 
hoelzl 
Moved Convex theory to library.

file 
diff 
annotate

Thu, 29 Apr 2010 11:41:04 0700 
huffman 
define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general

file 
diff 
annotate

Thu, 29 Apr 2010 07:22:01 0700 
huffman 
remove redundant constants pastecart, fstcart, sndcart; users should prefer Pair, fst, snd instead

file 
diff 
annotate

Wed, 28 Apr 2010 17:48:59 0700 
huffman 
prove lemma openin_subopen without using choice

file 
diff 
annotate

Tue, 27 Apr 2010 10:54:24 0700 
huffman 
generalize more continuity lemmas

file 
diff 
annotate

Tue, 27 Apr 2010 10:39:52 0700 
huffman 
generalized many lemmas about continuity

file 
diff 
annotate

Mon, 26 Apr 2010 22:21:03 0700 
huffman 
simplify definition of continuous_on; generalize some lemmas

file 
diff 
annotate

Mon, 26 Apr 2010 20:03:01 0700 
huffman 
move intervals section heading

file 
diff 
annotate

Mon, 26 Apr 2010 19:58:51 0700 
huffman 
remove unused, redundant constant inv_on

file 
diff 
annotate

Mon, 26 Apr 2010 19:55:50 0700 
huffman 
reorganize subsection headings

file 
diff 
annotate

Mon, 26 Apr 2010 12:19:57 0700 
huffman 
move definitions and theorems for type real^1 to separate theory file

file 
diff 
annotate

Mon, 26 Apr 2010 09:45:22 0700 
huffman 
merged

file 
diff 
annotate

Mon, 26 Apr 2010 09:21:25 0700 
huffman 
fix lots of looping simp calls and other warnings

file 
diff 
annotate

Sun, 25 Apr 2010 20:48:19 0700 
huffman 
define finerthan ordering on net type; move some theorems into Limits.thy

file 
diff 
annotate

Sun, 25 Apr 2010 16:23:40 0700 
huffman 
generalize type of continuous_on

file 
diff 
annotate

Sun, 25 Apr 2010 11:58:39 0700 
huffman 
define nets directly as filters, instead of as filter bases

file 
diff 
annotate

Mon, 26 Apr 2010 11:34:19 +0200 
haftmann 
dropped group_simps, ring_simps, field_eq_simps

file 
diff 
annotate

Sat, 24 Apr 2010 14:06:19 0700 
huffman 
minimize imports

file 
diff 
annotate

Thu, 18 Mar 2010 13:56:33 +0100 
haftmann 
dropped odd interpretation of comm_monoid_mult into comm_monoid_add; consider Min.insert_idem as default simp rule

file 
diff 
annotate

Wed, 17 Feb 2010 18:33:45 +0100 
himmelma 
Added integration to MultivariateAnalysis (upto FTC)

file 
diff 
annotate

Fri, 05 Feb 2010 14:33:50 +0100 
haftmann 
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS

file 
diff 
annotate

Thu, 04 Feb 2010 14:45:08 +0100 
hoelzl 
Changed 'bounded unique existential quantifiers' from a constant to syntax translation.

file 
diff 
annotate

Mon, 25 Jan 2010 16:56:24 +0100 
hoelzl 
Replaced vec1 and dest_vec1 by abbreviation.

file 
diff 
annotate

Thu, 07 Jan 2010 18:56:39 +0100 
hoelzl 
finite annotation on cartesian product is now implicit.

file 
diff 
annotate

Wed, 06 Jan 2010 13:07:30 +0100 
himmelma 
Made finite cartesian products finite

file 
diff 
annotate

Mon, 23 Nov 2009 15:30:32 0800 
huffman 
replace 'UNIV  S' with ' S'

file 
diff 
annotate

Tue, 24 Nov 2009 10:14:59 0800 
huffman 
restate lemmas using 'range'

file 
diff 
annotate

Thu, 19 Nov 2009 11:51:37 +0100 
hoelzl 
Renamed vector_less_eq_def to the more usual name vector_le_def.

file 
diff 
annotate

Mon, 16 Nov 2009 15:03:23 +0100 
hoelzl 
removed hassize predicate

file 
diff 
annotate

Mon, 16 Nov 2009 15:06:34 +0100 
hoelzl 
Added new lemmas to Euclidean Space by Robert Himmelmann

file 
diff 
annotate

Thu, 29 Oct 2009 16:21:43 +0000 
paulson 
Tidied up some very ugly proofs

file 
diff 
annotate

Tue, 27 Oct 2009 14:46:03 +0000 
paulson 
merged

file 
diff 
annotate

Fri, 23 Oct 2009 13:23:18 +0200 
himmelma 
distinguished session for multivariate analysis

file 
diff 
annotate
