| Tue, 27 Oct 2009 12:59:57 +0000 |
paulson |
New theory SupInf of the supremum and infimum operators for sets of reals.
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Mon, 31 Aug 2009 14:09:42 +0200 |
nipkow |
tuned the simp rules for Int involving insert and intervals.
|
file |
diff |
annotate
|
| Sat, 13 Jun 2009 17:31:56 -0700 |
huffman |
generalize many constants and lemmas from Convex_Euclidean_Space
|
file |
diff |
annotate
|
| Sat, 13 Jun 2009 11:56:41 -0700 |
huffman |
replace uses of (bi)linear with bounded_(bi)linear
|
file |
diff |
annotate
|
| Fri, 12 Jun 2009 22:20:36 -0700 |
huffman |
replace all occurrences of dot at type real^'n with inner
|
file |
diff |
annotate
|
| Fri, 12 Jun 2009 12:00:30 -0700 |
huffman |
remove simp add: norm_scaleR
|
file |
diff |
annotate
|
| Fri, 12 Jun 2009 11:23:37 -0700 |
huffman |
replace all occurrences of 'op *s' at type real^'n with scaleR
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 20:04:55 -0700 |
huffman |
move lemma compact_Times; generalize more lemmas
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 11:51:12 -0700 |
huffman |
theorem attribute [tendsto_intros]
|
file |
diff |
annotate
|
| Wed, 10 Jun 2009 15:32:02 -0700 |
huffman |
rewrite proof of compact_convex_combinations to avoid pastecart and vec1
|
file |
diff |
annotate
|
| Tue, 09 Jun 2009 16:13:18 -0700 |
huffman |
remove uses of vec1 in continuity lemmas
|
file |
diff |
annotate
|
| Tue, 09 Jun 2009 11:12:08 -0700 |
huffman |
merged
|
file |
diff |
annotate
|
| Mon, 08 Jun 2009 17:15:22 -0700 |
huffman |
generalize constant 'bounded' to class metric_space
|
file |
diff |
annotate
|
| Tue, 09 Jun 2009 16:38:33 +0200 |
himmelma |
removed duplicate lemmas
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 14:32:00 -0700 |
huffman |
generalize norm method to work over class real_normed_vector
|
file |
diff |
annotate
|
| Wed, 03 Jun 2009 10:02:59 -0700 |
huffman |
generalize some constants and lemmas to class topological_space
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 23:56:12 -0700 |
huffman |
merged
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 22:09:50 -0700 |
huffman |
generalize more constants
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 10:04:03 +0200 |
berghofe |
merged
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 10:02:08 +0200 |
berghofe |
Enclosed parts of subsection in @{text ...} to make LaTeX happy.
|
file |
diff |
annotate
|
| Fri, 29 May 2009 22:42:13 -0700 |
huffman |
generalize at function to class perfect_space
|
file |
diff |
annotate
|
| Fri, 29 May 2009 18:23:07 -0700 |
huffman |
generalize topological notions to class metric_space; add class perfect_space
|
file |
diff |
annotate
|
| Thu, 28 May 2009 17:00:02 -0700 |
huffman |
move dist operation to new metric_space class
|
file |
diff |
annotate
|
| Thu, 28 May 2009 13:43:45 -0700 |
huffman |
merged
|
file |
diff |
annotate
|
| Thu, 28 May 2009 13:41:41 -0700 |
huffman |
generalize dist function to class real_normed_vector
|
file |
diff |
annotate
|
| Thu, 28 May 2009 16:19:34 +0200 |
himmelma |
Corrected definition of is_interval
|
file |
diff |
annotate
|
| Thu, 28 May 2009 15:42:44 +0200 |
himmelma |
Corrected error in Convex_Euclidean_Space
|
file |
diff |
annotate
|
| Thu, 28 May 2009 13:56:50 +0200 |
himmelma |
Added Convex_Euclidean_Space to Library.thy and Library/IsaMakefile
|
file |
diff |
annotate
|
| Thu, 28 May 2009 09:46:45 +0200 |
himmelma |
Added Convex_Euclidean_Space.thy
|
file |
diff |
annotate
|