| Sat, 13 Jun 2009 17:31:24 -0700 |
huffman |
generalize lemma connected_real_lemma
|
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 16:23:07 -0700 |
huffman |
declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
|
file |
diff |
annotate
|
| Fri, 12 Jun 2009 12:00:30 -0700 |
huffman |
remove simp add: norm_scaleR
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 16:26:06 -0700 |
huffman |
add lemmas about closed sets
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 12:05:41 -0700 |
huffman |
new lemmas
|
file |
diff |
annotate
|
| Tue, 09 Jun 2009 11:12:08 -0700 |
huffman |
merged
|
file |
diff |
annotate
|
| Mon, 08 Jun 2009 14:28:09 -0700 |
huffman |
lemmas about linear, bilinear
|
file |
diff |
annotate
|
| Tue, 09 Jun 2009 16:38:33 +0200 |
himmelma |
removed duplicate lemmas
|
file |
diff |
annotate
|
| Sun, 07 Jun 2009 19:38:32 -0700 |
huffman |
new setL2 lemmas; instance ^ :: (topological_space, finite) topological_space
|
file |
diff |
annotate
|
| Sun, 07 Jun 2009 17:59:54 -0700 |
huffman |
replace 'topo' with 'open'; add extra type constraint for 'open'
|
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 09:58:11 -0700 |
huffman |
replace class open with class topo
|
file |
diff |
annotate
|
| Wed, 03 Jun 2009 08:46:13 -0700 |
huffman |
open_dist instance for vectors
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 23:49:46 -0700 |
huffman |
instance ^ :: complete_space
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 20:10:56 -0700 |
huffman |
generalize lemma norm_pastecart
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 19:42:44 -0700 |
huffman |
generalize lemma norm_triangle_sub
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 10:32:19 -0700 |
huffman |
new lemmas
|
file |
diff |
annotate
|
| Fri, 29 May 2009 15:32:33 -0700 |
huffman |
instance ^ :: (metric_space, finite) metric_space
|
file |
diff |
annotate
|
| Fri, 29 May 2009 10:02:47 -0700 |
huffman |
fix reference to LIM_def
|
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
|
| Thu, 28 May 2009 09:46:43 +0200 |
himmelma |
Changed prioriy of vector_scalar_mult
|
file |
diff |
annotate
|
| Tue, 12 May 2009 17:32:49 +0100 |
chaieb |
Isolated decision procedure for noms and the general arithmetic solver
|
file |
diff |
annotate
|
| Mon, 04 May 2009 14:49:49 +0200 |
haftmann |
dropped duplicate lemma sum_nonneg_eq_zero_iff
|
file |
diff |
annotate
|
| Wed, 29 Apr 2009 14:20:26 +0200 |
haftmann |
farewell to class recpower
|
file |
diff |
annotate
|
| Wed, 22 Apr 2009 19:09:21 +0200 |
haftmann |
power operation defined generic
|
file |
diff |
annotate
|
| Mon, 23 Mar 2009 08:16:24 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 23 Mar 2009 08:14:23 +0100 |
haftmann |
tuned header
|
file |
diff |
annotate
|
| Sun, 22 Mar 2009 20:46:11 +0100 |
haftmann |
tuned header
|
file |
diff |
annotate
|
| Thu, 19 Mar 2009 01:29:19 -0700 |
huffman |
imported patch euclidean
|
file |
diff |
annotate
|
| Mon, 16 Mar 2009 18:24:30 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 19:58:26 +0100 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 09:27:23 -0700 |
huffman |
remove trailing spaces
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 08:24:28 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 08:23:10 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 23:52:47 +0100 |
wenzelm |
removed old/broken CVS Ids;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 19:21:56 +0000 |
chaieb |
fixed proofs; added rules as default simp-rules
|
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 08:52:44 -0800 |
huffman |
remove duplicate instance declaration
|
file |
diff |
annotate
|
| Sat, 21 Feb 2009 15:39:59 -0800 |
huffman |
real_inner class instance for vectors
|
file |
diff |
annotate
|
| Sat, 21 Feb 2009 11:18:50 -0800 |
huffman |
remove duplicated lemmas about norm
|
file |
diff |
annotate
|
| Sat, 21 Feb 2009 10:58:25 -0800 |
huffman |
real_normed_vector instance
|
file |
diff |
annotate
|
| Sat, 21 Feb 2009 09:55:32 -0800 |
huffman |
fix real_vector, real_algebra instances
|
file |
diff |
annotate
|
| Fri, 13 Feb 2009 14:45:10 -0800 |
huffman |
section -> subsection
|
file |
diff |
annotate
|
| Fri, 13 Feb 2009 14:41:54 -0800 |
huffman |
add instance for cancel_comm_monoid_add
|
file |
diff |
annotate
|
| Thu, 12 Feb 2009 12:35:45 -0800 |
huffman |
fix document generation
|
file |
diff |
annotate
|
| Mon, 09 Feb 2009 17:08:49 +0000 |
chaieb |
fixed proof -- removed unnecessary sorry
|
file |
diff |
annotate
|
| Mon, 09 Feb 2009 16:54:03 +0000 |
chaieb |
(Real) Vectors in Euclidean space, and elementary linear algebra.
|
file |
diff |
annotate
|