| Tue, 26 Mar 2013 12:20:57 +0100 |
hoelzl |
rename RealVector.thy to Real_Vector_Spaces.thy
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move connected to HOL image; used to show intermediate value theorem
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
|
file |
diff |
annotate
|
| Fri, 18 Jan 2013 20:31:22 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 18 Jan 2013 18:46:52 +0100 |
wenzelm |
tuned proof -- much faster;
|
file |
diff |
annotate
|
| Fri, 18 Jan 2013 20:01:59 +0100 |
hoelzl |
generalized diameter from real_normed_vector to metric_space
|
file |
diff |
annotate
|
| Thu, 10 Jan 2013 14:40:19 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 14 Dec 2012 15:46:01 +0100 |
hoelzl |
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
|
file |
diff |
annotate
|
| Fri, 16 Nov 2012 18:45:57 +0100 |
hoelzl |
move theorems to be more generally useable
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| Sat, 22 Sep 2012 20:38:42 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sat, 22 Sep 2012 20:37:47 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 22 Sep 2012 20:29:28 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 23:07:01 +0200 |
krauss |
Set_Algebras: removed syntax \<oplus> and \<otimes>, in favour of plain + and *
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 22:55:11 +0200 |
krauss |
removed "setsum_set", now subsumed by generic setsum
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Mon, 14 Nov 2011 09:49:05 +0100 |
huffman |
avoid numeral-representation-specific rules in metis proof
|
file |
diff |
annotate
|
| Thu, 22 Sep 2011 14:12:16 -0700 |
huffman |
discontinued legacy theorem names from RealDef.thy
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 09:02:58 -0700 |
huffman |
avoid using legacy theorem names
|
file |
diff |
annotate
|
| Thu, 01 Sep 2011 09:02:14 -0700 |
huffman |
modernize lemmas about 'continuous' and 'continuous_on';
|
file |
diff |
annotate
|
| Wed, 31 Aug 2011 13:51:22 -0700 |
huffman |
remove redundant lemma card_enum
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 19:41:38 -0700 |
huffman |
replace some continuous_on lemmas with more general versions
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 14:25:19 -0700 |
huffman |
generalize lemma finite_imp_compact_convex_hull and related lemmas
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 13:48:11 -0700 |
huffman |
generalize some lemmas
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 12:52:10 -0700 |
huffman |
generalize lemma convex_cone_hull
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 12:43:55 -0700 |
huffman |
rename subset_{interior,closure} to {interior,closure}_mono;
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 09:17:02 -0700 |
huffman |
simplify definition of 'interior';
|
file |
diff |
annotate
|
| Wed, 24 Aug 2011 09:08:00 -0700 |
huffman |
change some subsection headings to subsubsection
|
file |
diff |
annotate
|
| Tue, 23 Aug 2011 16:47:48 -0700 |
huffman |
remove unnecessary lemma card_ge1
|
file |
diff |
annotate
|