| 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
|