| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Fri, 09 Dec 2011 11:31:13 +0100 |
noschinl |
more systematic lemma name
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 17:44:41 +0100 |
wenzelm |
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 23:41:16 +0200 |
wenzelm |
tuned Named_Thms: proper binding;
|
file |
diff |
annotate
|
| Thu, 22 Sep 2011 14:12:16 -0700 |
huffman |
discontinued legacy theorem names from RealDef.thy
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 17:07:33 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Sun, 28 Aug 2011 09:20:12 -0700 |
huffman |
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 18:06:27 -0700 |
huffman |
remove redundant lemma lemma_DERIV_subst in favor of DERIV_cong
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 15:54:43 -0700 |
huffman |
Lim.thy: legacy theorems
|
file |
diff |
annotate
|
| Tue, 16 Aug 2011 09:31:23 -0700 |
huffman |
add simp rules for isCont
|
file |
diff |
annotate
|
| Mon, 15 Aug 2011 09:08:17 -0700 |
huffman |
simplify some proofs
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 16:57:37 -0700 |
huffman |
remove duplicate lemmas
|
file |
diff |
annotate
|
| Fri, 14 Jan 2011 15:44:47 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 15:00:59 +0100 |
hoelzl |
use DERIV_intros
|
file |
diff |
annotate
|
| Tue, 20 Jul 2010 06:35:29 +0200 |
haftmann |
robustified metis proof
|
file |
diff |
annotate
|
| Mon, 19 Jul 2010 20:19:03 +0200 |
haftmann |
diff_eq_diff_less_eq' replaces diff_eq_diff_less_eq
|
file |
diff |
annotate
|
| Mon, 19 Jul 2010 16:09:44 +0200 |
haftmann |
diff_minus subsumes diff_def
|
file |
diff |
annotate
|
| Sun, 09 May 2010 17:47:43 -0700 |
huffman |
avoid using real-specific versions of generic lemmas
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 14:21:44 -0800 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
| Sat, 16 Jan 2010 17:15:28 +0100 |
haftmann |
dropped some old primrecs and some constdefs
|
file |
diff |
annotate
|
| Sun, 15 Nov 2009 00:34:21 +0100 |
wenzelm |
simplified bulky metis proofs;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 15:38:45 +0100 |
wenzelm |
more "anti_sym" -> "antisym" (cf. a4179bf442d1);
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 11:33:33 +0000 |
paulson |
A number of theorems contributed by Jeremy Avigad
|
file |
diff |
annotate
|
| Thu, 02 Jul 2009 17:34:14 +0200 |
wenzelm |
renamed NamedThmsFun to Named_Thms;
|
file |
diff |
annotate
|
| Thu, 02 Jul 2009 15:37:22 +0200 |
wenzelm |
fixed document (DERIV_intros);
|
file |
diff |
annotate
|
| Tue, 30 Jun 2009 18:16:22 +0200 |
hoelzl |
Added DERIV_intros
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 23:31:03 -0700 |
huffman |
generalize type of constant lim
|
file |
diff |
annotate
|
| Fri, 29 May 2009 09:22:56 -0700 |
huffman |
generalize constants from Lim.thy to class metric_space
|
file |
diff |
annotate
|
| Thu, 28 May 2009 22:57:17 -0700 |
huffman |
generalize constants in SEQ.thy to class metric_space
|
file |
diff |
annotate
|