| Tue, 05 Nov 2013 09:45:02 +0100 |
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
|
file | diff | annotate |
| Tue, 05 Nov 2013 09:44:58 +0100 |
use bdd_above and bdd_below for conditionally complete lattices
|
file | diff | annotate |
| Fri, 01 Nov 2013 18:51:14 +0100 |
more simplification rules on unary and binary minus
|
file | diff | annotate |
| Fri, 13 Sep 2013 14:57:20 -0700 |
tuned proofs about 'convex'
|
file | diff | annotate |
| Fri, 13 Sep 2013 11:16:13 -0700 |
generalized and simplified proofs of several theorems about convex sets
|
file | diff | annotate |
| Thu, 12 Sep 2013 18:09:17 -0700 |
make 'linear' into a sublocale of 'bounded_linear';
|
file | diff | annotate |
| Wed, 04 Sep 2013 17:36:37 +0200 |
tuned proofs;
|
file | diff | annotate |
| Tue, 03 Sep 2013 01:12:40 +0200 |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file | diff | annotate |
| Sat, 31 Aug 2013 22:18:51 +0200 |
tuned proofs;
|
file | diff | annotate |
| Sat, 31 Aug 2013 18:12:51 +0200 |
tuned proofs;
|
file | diff | annotate |
| Sat, 31 Aug 2013 00:39:59 +0200 |
tuned proofs;
|
file | diff | annotate |
| Fri, 30 Aug 2013 18:22:17 +0200 |
tuned proofs;
|
file | diff | annotate |
| Fri, 30 Aug 2013 00:11:01 +0200 |
tuned proofs;
|
file | diff | annotate |
| Sun, 18 Aug 2013 19:59:19 +0200 |
more symbols;
|
file | diff | annotate |
| Tue, 13 Aug 2013 16:25:47 +0200 |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file | diff | annotate |
| Tue, 26 Mar 2013 12:20:57 +0100 |
rename RealVector.thy to Real_Vector_Spaces.thy
|
file | diff | annotate |
| Fri, 22 Mar 2013 10:41:43 +0100 |
move connected to HOL image; used to show intermediate value theorem
|
file | diff | annotate |
| Fri, 22 Mar 2013 10:41:43 +0100 |
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 |
merged
|
file | diff | annotate |
| Fri, 18 Jan 2013 18:46:52 +0100 |
tuned proof -- much faster;
|
file | diff | annotate |
| Fri, 18 Jan 2013 20:01:59 +0100 |
generalized diameter from real_normed_vector to metric_space
|
file | diff | annotate |
| Thu, 10 Jan 2013 14:40:19 +0100 |
tuned proofs;
|
file | diff | annotate |
| Fri, 14 Dec 2012 15:46:01 +0100 |
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 |
move theorems to be more generally useable
|
file | diff | annotate |
| Fri, 19 Oct 2012 15:12:52 +0200 |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file | diff | annotate |
| Sat, 22 Sep 2012 20:38:42 +0200 |
tuned whitespace;
|
file | diff | annotate |
| Sat, 22 Sep 2012 20:37:47 +0200 |
tuned;
|
file | diff | annotate |
| Sat, 22 Sep 2012 20:29:28 +0200 |
tuned proofs;
|
file | diff | annotate |
| Thu, 12 Apr 2012 23:07:01 +0200 |
Set_Algebras: removed syntax \<oplus> and \<otimes>, in favour of plain + and *
|
file | diff | annotate |
| Thu, 12 Apr 2012 22:55:11 +0200 |
removed "setsum_set", now subsumed by generic setsum
|
file | diff | annotate |
| Sun, 25 Mar 2012 20:15:39 +0200 |
merged fork with new numeral representation (see NEWS)
|
file | diff | annotate |
| Mon, 14 Nov 2011 09:49:05 +0100 |
avoid numeral-representation-specific rules in metis proof
|
file | diff | annotate |
| Thu, 22 Sep 2011 14:12:16 -0700 |
discontinued legacy theorem names from RealDef.thy
|
file | diff | annotate |
| Mon, 12 Sep 2011 07:55:43 +0200 |
new fastforce replacing fastsimp - less confusing name
|
file | diff | annotate |
| Wed, 07 Sep 2011 09:02:58 -0700 |
avoid using legacy theorem names
|
file | diff | annotate |
| Thu, 01 Sep 2011 09:02:14 -0700 |
modernize lemmas about 'continuous' and 'continuous_on';
|
file | diff | annotate |
| Wed, 31 Aug 2011 13:51:22 -0700 |
remove redundant lemma card_enum
|
file | diff | annotate |
| Thu, 25 Aug 2011 19:41:38 -0700 |
replace some continuous_on lemmas with more general versions
|
file | diff | annotate |
| Thu, 25 Aug 2011 14:25:19 -0700 |
generalize lemma finite_imp_compact_convex_hull and related lemmas
|
file | diff | annotate |
| Thu, 25 Aug 2011 13:48:11 -0700 |
generalize some lemmas
|
file | diff | annotate |
| Thu, 25 Aug 2011 12:52:10 -0700 |
generalize lemma convex_cone_hull
|
file | diff | annotate |
| Thu, 25 Aug 2011 12:43:55 -0700 |
rename subset_{interior,closure} to {interior,closure}_mono;
|
file | diff | annotate |
| Thu, 25 Aug 2011 09:17:02 -0700 |
simplify definition of 'interior';
|
file | diff | annotate |
| Wed, 24 Aug 2011 09:08:00 -0700 |
change some subsection headings to subsubsection
|
file | diff | annotate |
| Tue, 23 Aug 2011 16:47:48 -0700 |
remove unnecessary lemma card_ge1
|
file | diff | annotate |
| Tue, 23 Aug 2011 16:17:22 -0700 |
move connected_real_lemma to the one place it is used
|
file | diff | annotate |
| Tue, 23 Aug 2011 14:11:02 -0700 |
declare euclidean_simps [simp] at the point they are proved;
|
file | diff | annotate |
| Sun, 21 Aug 2011 12:22:31 -0700 |
add lemmas interior_Times and closure_Times
|
file | diff | annotate |
| Sun, 21 Aug 2011 11:03:15 -0700 |
remove unnecessary euclidean_space class constraints
|
file | diff | annotate |
| Sat, 20 Aug 2011 15:54:26 -0700 |
remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff
|
file | diff | annotate |
| Thu, 18 Aug 2011 13:36:58 -0700 |
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
|
file | diff | annotate |
| Fri, 12 Aug 2011 09:17:24 -0700 |
make Multivariate_Analysis work with separate set type
|
file | diff | annotate |
| Wed, 10 Aug 2011 18:02:16 -0700 |
avoid warnings about duplicate rules
|
file | diff | annotate |
| Wed, 10 Aug 2011 08:42:26 -0700 |
full import paths
|
file | diff | annotate |
| Tue, 09 Aug 2011 10:30:00 -0700 |
mark some redundant theorems as legacy
|
file | diff | annotate |
| Sat, 30 Jul 2011 08:24:46 +0200 |
tuned proofs
|
file | diff | annotate |
| Mon, 25 Jul 2011 23:26:55 +0200 |
adjusted to tailored version of ball_simps
|
file | diff | annotate |
| Sun, 13 Mar 2011 22:55:50 +0100 |
tuned headers;
|
file | diff | annotate |
| Wed, 29 Dec 2010 17:34:41 +0100 |
explicit file specifications -- avoid secondary load path;
|
file | diff | annotate |
| Fri, 03 Dec 2010 00:36:01 +0100 |
adapt proofs to changed set_plus_image (cf. ee8d0548c148);
|
file | diff | annotate |