Fri, 08 Mar 2013 11:28:04 +0100 simplified basic termination proof
nipkow [Fri, 08 Mar 2013 11:28:04 +0100] rev 51372
simplified basic termination proof
Fri, 08 Mar 2013 09:34:38 +0100 some simp rules for fset
traytel [Fri, 08 Mar 2013 09:34:38 +0100] rev 51371
some simp rules for fset
Thu, 07 Mar 2013 18:14:30 +0100 avoid -Infinity which confuses JFreeChart histogram;
wenzelm [Thu, 07 Mar 2013 18:14:30 +0100] rev 51370
avoid -Infinity which confuses JFreeChart histogram;
Thu, 07 Mar 2013 17:50:26 +0100 tuned proofs -- more structure, less warnings;
wenzelm [Thu, 07 Mar 2013 17:50:26 +0100] rev 51369
tuned proofs -- more structure, less warnings;
Thu, 07 Mar 2013 15:02:55 +0100 tuned signature -- prefer terminology of Scala and Axiom;
wenzelm [Thu, 07 Mar 2013 15:02:55 +0100] rev 51368
tuned signature -- prefer terminology of Scala and Axiom;
Thu, 07 Mar 2013 13:44:54 +0100 better message (type-unsoundnesses are becoming rare, usually the issue is elsewhere, e.g. in the TSTP proof parser)
blanchet [Thu, 07 Mar 2013 13:44:54 +0100] rev 51367
better message (type-unsoundnesses are becoming rare, usually the issue is elsewhere, e.g. in the TSTP proof parser)
Wed, 06 Mar 2013 10:44:43 -0800 avoid using Arith_Data.dest_sum in extended-nat simprocs (it treats 'x - y' as 'x + - y', which is not valid for enat)
huffman [Wed, 06 Mar 2013 10:44:43 -0800] rev 51366
avoid using Arith_Data.dest_sum in extended-nat simprocs (it treats 'x - y' as 'x + - y', which is not valid for enat)
Wed, 06 Mar 2013 16:56:21 +0100 netlimit is abbreviation for Lim
hoelzl [Wed, 06 Mar 2013 16:56:21 +0100] rev 51365
netlimit is abbreviation for Lim
Wed, 06 Mar 2013 16:56:21 +0100 tuned proofs
hoelzl [Wed, 06 Mar 2013 16:56:21 +0100] rev 51364
tuned proofs
Wed, 06 Mar 2013 16:56:21 +0100 changed has_derivative_intros into a named theorems collection
hoelzl [Wed, 06 Mar 2013 16:56:21 +0100] rev 51363
changed has_derivative_intros into a named theorems collection
Wed, 06 Mar 2013 16:56:21 +0100 changed continuous_on_intros into a named theorems collection
hoelzl [Wed, 06 Mar 2013 16:56:21 +0100] rev 51362
changed continuous_on_intros into a named theorems collection
Wed, 06 Mar 2013 16:56:21 +0100 changed continuous_intros into a named theorems collection
hoelzl [Wed, 06 Mar 2013 16:56:21 +0100] rev 51361
changed continuous_intros into a named theorems collection
Wed, 06 Mar 2013 16:56:21 +0100 add tendsto_eq_intros: they add an additional rewriting step at the rhs of --->
hoelzl [Wed, 06 Mar 2013 16:56:21 +0100] rev 51360
add tendsto_eq_intros: they add an additional rewriting step at the rhs of --->
Wed, 06 Mar 2013 16:10:56 +0100 major redesign: order instead of preorder, new definition of intervals as quotients
nipkow [Wed, 06 Mar 2013 16:10:56 +0100] rev 51359
major redesign: order instead of preorder, new definition of intervals as quotients
Wed, 06 Mar 2013 14:10:07 +0100 added lemma
nipkow [Wed, 06 Mar 2013 14:10:07 +0100] rev 51358
added lemma
Wed, 06 Mar 2013 12:17:52 +0100 extended numerals
nipkow [Wed, 06 Mar 2013 12:17:52 +0100] rev 51357
extended numerals
Tue, 05 Mar 2013 17:25:41 +0100 merged
wenzelm [Tue, 05 Mar 2013 17:25:41 +0100] rev 51356
merged
Tue, 05 Mar 2013 17:07:36 +0100 merged
wenzelm [Tue, 05 Mar 2013 17:07:36 +0100] rev 51355
merged
Tue, 05 Mar 2013 11:37:01 +0100 removed unused Future.flat, while leaving its influence of Future.map (see bcd6b1aa4db5);
wenzelm [Tue, 05 Mar 2013 11:37:01 +0100] rev 51354
removed unused Future.flat, while leaving its influence of Future.map (see bcd6b1aa4db5);
Tue, 05 Mar 2013 17:18:02 +0100 extended stream library a little more
traytel [Tue, 05 Mar 2013 17:18:02 +0100] rev 51353
extended stream library a little more
Tue, 05 Mar 2013 17:10:49 +0100 extended stream library
traytel [Tue, 05 Mar 2013 17:10:49 +0100] rev 51352
extended stream library
Tue, 05 Mar 2013 15:43:22 +0100 generalized lemmas in Extended_Real_Limits
hoelzl [Tue, 05 Mar 2013 15:43:22 +0100] rev 51351
generalized lemmas in Extended_Real_Limits
Tue, 05 Mar 2013 15:43:21 +0100 eventually nhds represented using sequentially
hoelzl [Tue, 05 Mar 2013 15:43:21 +0100] rev 51350
eventually nhds represented using sequentially
Tue, 05 Mar 2013 15:43:20 +0100 generalized compact_Times to topological_space
hoelzl [Tue, 05 Mar 2013 15:43:20 +0100] rev 51349
generalized compact_Times to topological_space
Tue, 05 Mar 2013 15:43:19 +0100 move lemma Inf to usage point
hoelzl [Tue, 05 Mar 2013 15:43:19 +0100] rev 51348
move lemma Inf to usage point
Tue, 05 Mar 2013 15:43:18 +0100 tuned proof of Edelstein fixed point theorem (use continuity of dist and attains_sup)
hoelzl [Tue, 05 Mar 2013 15:43:18 +0100] rev 51347
tuned proof of Edelstein fixed point theorem (use continuity of dist and attains_sup)
Tue, 05 Mar 2013 15:43:17 +0100 tuned proofs (used continuity of infdist, dist and continuous_attains_sup)
hoelzl [Tue, 05 Mar 2013 15:43:17 +0100] rev 51346
tuned proofs (used continuity of infdist, dist and continuous_attains_sup)
Tue, 05 Mar 2013 15:43:16 +0100 generalized continuous/compact_attains_inf/sup from real to linorder_topology
hoelzl [Tue, 05 Mar 2013 15:43:16 +0100] rev 51345
generalized continuous/compact_attains_inf/sup from real to linorder_topology
Tue, 05 Mar 2013 15:43:15 +0100 continuity of pair operations
hoelzl [Tue, 05 Mar 2013 15:43:15 +0100] rev 51344
continuity of pair operations
Tue, 05 Mar 2013 15:43:14 +0100 use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl [Tue, 05 Mar 2013 15:43:14 +0100] rev 51343
use generate_topology for second countable topologies, does not require intersection stable basis
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 tip