| 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
|
| Wed, 28 Nov 2012 15:59:18 +0100 |
wenzelm |
eliminated slightly odd identifiers;
|
file |
diff |
annotate
|
| Tue, 27 Nov 2012 13:22:29 +0100 |
wenzelm |
eliminated some improper identifiers;
|
file |
diff |
annotate
|
| Fri, 16 Nov 2012 18:45:57 +0100 |
hoelzl |
move theorems to be more generally useable
|
file |
diff |
annotate
|
| Thu, 01 Nov 2012 13:32:57 +0100 |
blanchet |
regenerated SMT certificates
|
file |
diff |
annotate
|
| Mon, 22 Oct 2012 17:09:49 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2012 11:45:56 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 01 Oct 2012 17:29:00 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 07 Sep 2012 15:15:07 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 07 Sep 2012 13:58:43 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 04 Jun 2012 09:07:23 +0200 |
boehmes |
restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 15:15:00 +0200 |
huffman |
modernized obsolete old-style theory name with proper new-style underscore
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 16:59:13 +0300 |
blanchet |
renamed "smt_fixed" to "smt_read_only_certificates"
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 16:56:56 +0100 |
wenzelm |
prefer abs_def over def_raw;
|
file |
diff |
annotate
|
| Tue, 27 Dec 2011 09:45:10 +0100 |
haftmann |
be explicit about Finite_Set.fold
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 11:39:29 -0700 |
huffman |
simplify proofs using LIMSEQ lemmas
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 12:43:55 -0700 |
huffman |
rename subset_{interior,closure} to {interior,closure}_mono;
|
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 14:11:02 -0700 |
huffman |
declare euclidean_simps [simp] at the point they are 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 14:24:05 -0700 |
huffman |
avoid duplicate rule warnings
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 16:35:50 -0700 |
huffman |
remove several redundant and unused theorems about derivatives
|
file |
diff |
annotate
|
| Tue, 09 Aug 2011 10:30:00 -0700 |
huffman |
mark some redundant theorems as legacy
|
file |
diff |
annotate
|
| Fri, 20 May 2011 11:44:16 +0200 |
haftmann |
names of fold_set locales resemble name of characteristic property more closely
|
file |
diff |
annotate
|
| Fri, 20 May 2011 08:16:56 +0200 |
haftmann |
use point-free characterization for locale fun_left_comm_idem
|
file |
diff |
annotate
|
| Mon, 14 Mar 2011 14:37:33 +0100 |
hoelzl |
moved t2_spaces to HOL image
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 22:24:10 +0100 |
wenzelm |
eliminated hard tabs;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2011 10:55:41 +0100 |
hoelzl |
finally remove upper_bound_finite_set
|
file |
diff |
annotate
|
| Mon, 28 Feb 2011 22:10:57 +0100 |
boehmes |
removed dependency on Dense_Linear_Order
|
file |
diff |
annotate
|
| Fri, 25 Feb 2011 22:07:56 +0100 |
nipkow |
got rid of lemma upper_bound_finite_set
|
file |
diff |
annotate
|
| Mon, 17 Jan 2011 17:45:52 +0100 |
boehmes |
made Z3 the default SMT solver again
|
file |
diff |
annotate
|
| Thu, 06 Jan 2011 17:51:56 +0100 |
boehmes |
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
file |
diff |
annotate
|
| Fri, 12 Nov 2010 15:56:07 +0100 |
boehmes |
look for certificates relative to the theory
|
file |
diff |
annotate
|