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