| Wed, 03 Aug 2005 14:48:50 +0200 |
avigad |
renamed exp_ge_add_one_self to exp_ge_add_one_self_aux
|
file |
diff |
annotate
|
| Wed, 27 Jul 2005 11:28:18 +0200 |
paulson |
removed the dependence on abs_mult
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 19:49:07 +0200 |
avigad |
Additions to the Real (and Hyperreal) libraries:
|
file |
diff |
annotate
|
| Tue, 12 Jul 2005 17:56:03 +0200 |
avigad |
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
|
file |
diff |
annotate
|
| Fri, 01 Jul 2005 14:06:57 +0200 |
berghofe |
Simplified some proofs (thanks to strong_setsum_cong).
|
file |
diff |
annotate
|
| Wed, 02 Mar 2005 12:06:15 +0100 |
nipkow |
another reorganization of setsums and intervals
|
file |
diff |
annotate
|
| Wed, 23 Feb 2005 10:23:22 +0100 |
nipkow |
suminf -> \<Sum>
|
file |
diff |
annotate
|
| Tue, 22 Feb 2005 13:05:47 +0100 |
paulson |
removed redundant lemmas and simprules
|
file |
diff |
annotate
|
| Mon, 21 Feb 2005 19:23:46 +0100 |
nipkow |
more fine tuniung
|
file |
diff |
annotate
|
| Mon, 21 Feb 2005 15:04:10 +0100 |
nipkow |
comprehensive cleanup, replacing sumr by setsum
|
file |
diff |
annotate
|
| Fri, 18 Feb 2005 11:48:53 +0100 |
nipkow |
starting to get rid of sumr
|
file |
diff |
annotate
|
| Tue, 01 Feb 2005 18:01:57 +0100 |
paulson |
the new subst tactic, by Lucas Dixon
|
file |
diff |
annotate
|
| Tue, 07 Dec 2004 16:16:23 +0100 |
paulson |
made proofs more robust
|
file |
diff |
annotate
|
| Tue, 19 Oct 2004 18:18:45 +0200 |
paulson |
converted some induct_tac to induct
|
file |
diff |
annotate
|
| Tue, 12 Oct 2004 11:48:21 +0200 |
paulson |
tweaks concerned with poly bug-fixing
|
file |
diff |
annotate
|
| Thu, 07 Oct 2004 15:42:30 +0200 |
paulson |
simplification tweaks for better arithmetic reasoning
|
file |
diff |
annotate
|
| Tue, 05 Oct 2004 15:30:50 +0200 |
paulson |
new simprules for abs and for things like a/b<1
|
file |
diff |
annotate
|
| Mon, 04 Oct 2004 15:28:03 +0200 |
paulson |
revised simprules for division
|
file |
diff |
annotate
|
| Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
| Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
| Thu, 29 Jul 2004 16:57:41 +0200 |
paulson |
removal of more iff-rules from RealDef.thy
|
file |
diff |
annotate
|
| Thu, 29 Jul 2004 16:14:42 +0200 |
paulson |
removed some [iff] declarations from RealDef.thy, concerning inequalities
|
file |
diff |
annotate
|
| Wed, 28 Jul 2004 16:25:40 +0200 |
paulson |
abs notation
|
file |
diff |
annotate
|
| Wed, 28 Jul 2004 10:49:29 +0200 |
paulson |
conversion of Hyperreal/MacLaurin_lemmas to Isar script
|
file |
diff |
annotate
|
| Mon, 26 Jul 2004 17:34:52 +0200 |
paulson |
converting Hyperreal/Transcendental to Isar script
|
file |
diff |
annotate
|
| Thu, 01 Jul 2004 12:29:53 +0200 |
paulson |
new treatment of binary numerals
|
file |
diff |
annotate
|
| Mon, 05 May 2003 18:23:40 +0200 |
paulson |
New material on integration, etc. Moving Hyperreal/ex
|
file |
diff |
annotate
|
| Thu, 15 Nov 2001 16:12:49 +0100 |
paulson |
new theories from Jacques Fleuriot
|
file |
diff |
annotate
|