Mon, 09 May 2016 17:23:19 +0100 |
paulson |
lemmas about dimension, hyperplanes, span, etc.
|
file |
diff |
annotate
|
Mon, 09 May 2016 16:02:23 +0100 |
paulson |
renamings and refinements
|
file |
diff |
annotate
|
Fri, 22 Apr 2016 17:22:29 +0200 |
hoelzl |
Linear_Algebra: generalize linear_surjective_right/injective_left_inverse to real vector spaces
|
file |
diff |
annotate
|
Fri, 22 Apr 2016 15:18:46 +0200 |
hoelzl |
Linear_Algebra: generalize linear_independent_extend to all real vector spaces
|
file |
diff |
annotate
|
Fri, 22 Apr 2016 11:57:03 +0200 |
hoelzl |
Linear_Algebra: alternative representation of linear combination
|
file |
diff |
annotate
|
Fri, 22 Apr 2016 11:43:47 +0200 |
hoelzl |
Linear_Algebra: move abstract concepts to front
|
file |
diff |
annotate
|
Mon, 18 Apr 2016 14:30:32 +0100 |
paulson |
new theorems about convex hulls, etc.; also, renamed some theorems
|
file |
diff |
annotate
|
Mon, 11 Apr 2016 16:27:42 +0100 |
paulson |
lots of new theorems for multivariate analysis
|
file |
diff |
annotate
|
Tue, 15 Mar 2016 14:08:25 +0000 |
paulson |
rationalisation of theorem names esp about "real Archimedian" etc.
|
file |
diff |
annotate
|
Wed, 24 Feb 2016 15:51:01 +0000 |
paulson |
Substantial new material for multivariate analysis. Also removal of some duplicates.
|
file |
diff |
annotate
|
Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
Wed, 30 Dec 2015 11:21:54 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
Tue, 22 Dec 2015 21:58:27 +0100 |
immler |
theory for type of bounded linear functions; differentiation under the integral sign
|
file |
diff |
annotate
|
Mon, 07 Dec 2015 20:19:59 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
Tue, 10 Nov 2015 14:18:41 +0000 |
paulson |
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
|
file |
diff |
annotate
|
Tue, 27 Oct 2015 15:17:02 +0000 |
paulson |
Cauchy's integral formula, required lemmas, and a bit of reorganisation
|
file |
diff |
annotate
|
Mon, 26 Oct 2015 23:41:27 +0000 |
paulson |
new lemmas about topology, etc., for Cauchy integral formula
|
file |
diff |
annotate
|
Fri, 02 Oct 2015 15:07:41 +0100 |
paulson |
New theorems about connected sets. And pairwise moved to Set.thy.
|
file |
diff |
annotate
|
Wed, 30 Sep 2015 16:36:42 +0100 |
paulson |
real_of_nat_Suc is now a simprule
|
file |
diff |
annotate
|
Mon, 21 Sep 2015 21:46:14 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
Wed, 19 Aug 2015 19:18:19 +0100 |
paulson |
New material and fixes related to the forthcoming Stone-Weierstrass development
|
file |
diff |
annotate
|
Tue, 28 Jul 2015 17:15:01 +0100 |
paulson |
tweaks. Got rid of a really slow step
|
file |
diff |
annotate
|
Mon, 27 Jul 2015 16:52:57 +0100 |
paulson |
New material for Cauchy's integral theorem
|
file |
diff |
annotate
|
Mon, 20 Jul 2015 23:12:50 +0100 |
paulson |
new material for multivariate analysis, etc.
|
file |
diff |
annotate
|
Wed, 10 Jun 2015 19:10:20 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
Thu, 28 May 2015 14:33:35 +0100 |
paulson |
Convex hulls: theorems about interior, etc. And a few simple lemmas.
|
file |
diff |
annotate
|
Tue, 26 May 2015 21:58:04 +0100 |
paulson |
New material about paths, and some lemmas
|
file |
diff |
annotate
|
Thu, 30 Apr 2015 15:28:01 +0100 |
paulson |
tidying some messy proofs
|
file |
diff |
annotate
|
Tue, 28 Apr 2015 16:23:38 +0100 |
paulson |
New material about complex transcendental functions (especially Ln, Arg) and polynomials
|
file |
diff |
annotate
|
Tue, 31 Mar 2015 16:48:48 +0100 |
paulson |
rationalised and generalised some theorems concerning abs and x^2.
|
file |
diff |
annotate
|
Thu, 19 Feb 2015 11:53:36 +0100 |
haftmann |
establish unique preferred fact names
|
file |
diff |
annotate
|
Sun, 02 Nov 2014 17:09:04 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
Sat, 05 Jul 2014 11:01:53 +0200 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
file |
diff |
annotate
|
Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
Fri, 11 Apr 2014 13:36:57 +0200 |
nipkow |
made mult_nonneg_nonneg a simp rule
|
file |
diff |
annotate
|
Wed, 09 Apr 2014 09:37:48 +0200 |
hoelzl |
field_simps: better support for negation and division, and power
|
file |
diff |
annotate
|
Wed, 09 Apr 2014 09:37:47 +0200 |
hoelzl |
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
|
file |
diff |
annotate
|
Sun, 06 Apr 2014 19:35:35 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Thu, 03 Apr 2014 23:51:52 +0100 |
paulson |
removing simprule status for divide_minus_left and divide_minus_right
|
file |
diff |
annotate
|
Tue, 18 Mar 2014 09:39:07 -0700 |
huffman |
remove unnecessary finiteness assumptions from lemmas about setsum
|
file |
diff |
annotate
|
Sun, 16 Mar 2014 18:09:04 +0100 |
haftmann |
normalising simp rules for compound operators
|
file |
diff |
annotate
|
Tue, 04 Mar 2014 14:14:28 -0800 |
huffman |
tuned proof
|
file |
diff |
annotate
|
Thu, 27 Feb 2014 16:07:21 +0000 |
paulson |
A bit of tidying up
|
file |
diff |
annotate
|
Sat, 25 Jan 2014 16:45:13 +0100 |
wenzelm |
tuned proof;
|
file |
diff |
annotate
|
Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
summarized notions related to ordered_euclidean_space and intervals in separate theory
|
file |
diff |
annotate
|
Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
introduced ordered real vector spaces
|
file |
diff |
annotate
|
Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
|
file |
diff |
annotate
|
Mon, 09 Dec 2013 12:22:23 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
Tue, 12 Nov 2013 19:28:54 +0100 |
hoelzl |
add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image
|
file |
diff |
annotate
|
Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
Thu, 26 Sep 2013 16:33:34 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
Thu, 26 Sep 2013 16:33:32 -0700 |
huffman |
moved lemma
|
file |
diff |
annotate
|
Tue, 24 Sep 2013 16:03:00 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Wed, 18 Sep 2013 20:32:11 +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:33:36 -0700 |
huffman |
new lemmas
|
file |
diff |
annotate
|
Thu, 12 Sep 2013 09:06:46 -0700 |
huffman |
prefer theorem name over 'long_thm_list(n)'
|
file |
diff |
annotate
|
Wed, 04 Sep 2013 17:36:37 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Sun, 18 Aug 2013 19:59:19 +0200 |
wenzelm |
more symbols;
|
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
|
Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
|
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, 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 19:14:23 +0100 |
hoelzl |
moved (b)choice_iff(') to Hilbert_Choice
|
file |
diff |
annotate
|
Fri, 16 Nov 2012 18:45:57 +0100 |
hoelzl |
move theorems to be more generally useable
|
file |
diff |
annotate
|
Fri, 05 Oct 2012 13:57:48 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Sat, 29 Sep 2012 21:24:20 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Fri, 28 Sep 2012 23:02:49 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Sat, 22 Sep 2012 17:55:56 +0200 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
Fri, 21 Sep 2012 22:45:14 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
Tue, 06 Sep 2011 08:00:28 -0700 |
huffman |
remove duplicate copy of lemma sqrt_add_le_add_sqrt
|
file |
diff |
annotate
|
Tue, 06 Sep 2011 07:48:59 -0700 |
huffman |
remove redundant lemma real_sum_squared_expand in favor of power2_sum
|
file |
diff |
annotate
|
Fri, 02 Sep 2011 13:57:12 -0700 |
huffman |
remove more duplicate lemmas
|
file |
diff |
annotate
|
Thu, 01 Sep 2011 07:31:33 -0700 |
huffman |
add lemma tendsto_infnorm
|
file |
diff |
annotate
|
Wed, 31 Aug 2011 13:51:22 -0700 |
huffman |
remove redundant lemma card_enum
|
file |
diff |
annotate
|
Thu, 25 Aug 2011 16:42:13 -0700 |
huffman |
arrange everything related to ordered_euclidean_space class together
|
file |
diff |
annotate
|
Thu, 25 Aug 2011 16:06:50 -0700 |
huffman |
generalize and shorten proof of basis_orthogonal
|
file |
diff |
annotate
|
Thu, 25 Aug 2011 15:35:54 -0700 |
huffman |
remove dot_lsum and dot_rsum in favor of inner_setsum_{left,right}
|
file |
diff |
annotate
|
Thu, 25 Aug 2011 11:57:42 -0700 |
huffman |
simplify many proofs about subspace and span;
|
file |
diff |
annotate
|
Wed, 24 Aug 2011 15:32:40 -0700 |
huffman |
minimize imports
|
file |
diff |
annotate
|
Wed, 24 Aug 2011 15:06:13 -0700 |
huffman |
move everything related to 'norm' method into new theory file Norm_Arith.thy
|
file |
diff |
annotate
|
Wed, 24 Aug 2011 12:39:42 -0700 |
huffman |
remove unused lemmas dimensionI, dimension_eq
|
file |
diff |
annotate
|
Wed, 24 Aug 2011 11:56:57 -0700 |
huffman |
move geometric progression lemmas from Linear_Algebra.thy to Integration.thy where they are used
|
file |
diff |
annotate
|
Tue, 23 Aug 2011 16:17:22 -0700 |
huffman |
move connected_real_lemma to the one place it is used
|
file |
diff |
annotate
|
Tue, 23 Aug 2011 14:11:02 -0700 |
huffman |
declare euclidean_simps [simp] at the point they are proved;
|
file |
diff |
annotate
|
Mon, 22 Aug 2011 17:22:49 -0700 |
huffman |
avoid warnings
|
file |
diff |
annotate
|
Mon, 22 Aug 2011 10:19:39 -0700 |
huffman |
remove duplicate lemma
|
file |
diff |
annotate
|
Sun, 21 Aug 2011 09:46:20 -0700 |
huffman |
section -> subsection
|
file |
diff |
annotate
|
Thu, 18 Aug 2011 18:08:43 -0700 |
huffman |
import Library/Sum_of_Squares instead of reloading positivstellensatz.ML
|
file |
diff |
annotate
|
Thu, 18 Aug 2011 17:32:02 -0700 |
huffman |
declare euclidean_component_zero[simp] at the point it is proved
|
file |
diff |
annotate
|
Thu, 18 Aug 2011 13:36:58 -0700 |
huffman |
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
|
file |
diff |
annotate
|
Fri, 12 Aug 2011 20:55:22 -0700 |
huffman |
remove redundant lemma setsum_norm in favor of norm_setsum;
|
file |
diff |
annotate
|
Fri, 12 Aug 2011 09:17:24 -0700 |
huffman |
make Multivariate_Analysis work with separate set type
|
file |
diff |
annotate
|
Thu, 11 Aug 2011 13:05:56 -0700 |
huffman |
modify euclidean_space class to include basis set
|
file |
diff |
annotate
|
Wed, 10 Aug 2011 18:02:16 -0700 |
huffman |
avoid warnings about duplicate rules
|
file |
diff |
annotate
|
Wed, 10 Aug 2011 09:23:42 -0700 |
huffman |
split Linear_Algebra.thy from Euclidean_Space.thy
|
file |
diff |
annotate
|