| Wed, 03 Jun 2009 10:29:11 -0700 |
huffman |
more [code del] declarations
|
file |
diff |
annotate
|
| Wed, 03 Jun 2009 09:58:11 -0700 |
huffman |
replace class open with class topo
|
file |
diff |
annotate
|
| Wed, 03 Jun 2009 07:44:56 -0700 |
huffman |
introduce class topological_space as a superclass of metric_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:41:41 -0700 |
huffman |
generalize dist function to class real_normed_vector
|
file |
diff |
annotate
|
| Tue, 28 Apr 2009 15:50:30 +0200 |
haftmann |
stripped class recpower further
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 20:08:55 +0100 |
wenzelm |
interpretation/interpret: prefixes are mandatory by default;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 17:12:23 -0800 |
huffman |
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Sun, 22 Feb 2009 12:48:49 -0800 |
huffman |
declare scaleR distrib rules [algebra_simps]; cleaned up
|
file |
diff |
annotate
|
| Sun, 22 Feb 2009 12:16:51 -0800 |
huffman |
clean up instantiations
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:40:23 +0100 |
haftmann |
no base sort in class import
|
file |
diff |
annotate
|
| Tue, 30 Dec 2008 11:10:01 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
| base
|
| Mon, 29 Dec 2008 14:08:08 +0100 |
haftmann |
adapted HOL source structure to distribution layout
|
file |
diff |
annotate
| base
|