src/HOL/Complex/ex/ROOT.ML
Fri, 10 Aug 2007 15:28:11 +0200 wenzelm simultaneous use_thys;
Thu, 21 Jun 2007 15:42:07 +0200 wenzelm replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
Sun, 10 Jun 2007 21:06:59 +0200 wenzelm disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
Tue, 05 Jun 2007 20:44:12 +0200 chaieb Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
Tue, 16 May 2006 13:01:22 +0200 wenzelm added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
Wed, 26 Apr 2006 07:01:33 +0200 kleing moved arithmetic series to geometric series in SetInterval
Fri, 07 Apr 2006 12:48:10 +0200 kleing remame ASeries to Arithmetic_Series
Sun, 19 Feb 2006 22:40:18 +0100 kleing fixed document
Sun, 19 Feb 2006 22:12:30 +0100 kleing * denumerability of rationals by Benjamin Porter, based on NatPair (by Stefan Richter)
Sun, 19 Feb 2006 13:21:32 +0100 kleing * added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
Wed, 31 Aug 2005 15:46:35 +0200 wenzelm added Complex/ex/BigO_Complex.thy;
Tue, 06 May 2003 17:45:54 +0200 paulson removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
Mon, 05 May 2003 18:22:31 +0200 paulson new session Complex for the complex numbers
less more (0) tip