| Tue, 24 Sep 2013 16:03:00 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 14 Sep 2013 22:30:10 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 14 Sep 2013 13:59:57 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Thu, 12 Sep 2013 18:09:17 -0700 |
huffman |
make 'linear' into a sublocale of 'bounded_linear';
|
file |
diff |
annotate
|
| Thu, 12 Sep 2013 09:39:02 -0700 |
huffman |
remove duplicate lemmas
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 00:00:59 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 10 Sep 2013 23:50:03 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 10 Sep 2013 18:14:47 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 10 Sep 2013 00:18:30 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 09 Sep 2013 23:11:02 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 07 Sep 2013 23:09:26 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 06 Sep 2013 18:14:50 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 06 Sep 2013 17:55:01 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 06 Sep 2013 12:22:00 +0200 |
wenzelm |
removed junk;
|
file |
diff |
annotate
|
| Wed, 04 Sep 2013 23:57:38 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 04 Sep 2013 22:37:19 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 04 Sep 2013 21:25:03 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 04 Sep 2013 13:13:14 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:44:29 +0200 |
haftmann |
weaker precendence of syntax for big intersection and union on sets
|
file |
diff |
annotate
|
| Tue, 09 Apr 2013 14:04:47 +0200 |
hoelzl |
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 12:20:52 +0100 |
hoelzl |
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 20:50:39 +0100 |
haftmann |
fundamental revision of big operators on sets
|
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
|
| Tue, 05 Mar 2013 15:43:19 +0100 |
hoelzl |
move lemma Inf to usage point
|
file |
diff |
annotate
|
| Thu, 17 Jan 2013 15:17:48 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 16 Jan 2013 22:18:13 +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
|
| Tue, 04 Dec 2012 18:00:40 +0100 |
hoelzl |
remove SMT proofs in Multivariate_Analysis
|
file |
diff |
annotate
|