src/HOL/Complex/NSComplex.thy
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-07-29 paulson 2004-07-29 removed some [iff] declarations from RealDef.thy, concerning inequalities
2004-07-01 paulson 2004-07-01 new treatment of binary numerals
2004-06-24 paulson 2004-06-24 replaced monomorphic abs definitions by abs_if
2004-05-11 obua 2004-05-11 changes made due to new Ring_and_Field theory
2004-05-01 wenzelm 2004-05-01 tuned instance statements;
2004-04-23 paulson 2004-04-23 congruent2 now allows different equiv relations
2004-04-22 wenzelm 2004-04-22 constdefs: proper order;
2004-04-22 paulson 2004-04-22 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate places
2004-03-15 paulson 2004-03-15 heavy tidying
2004-03-08 paulson 2004-03-08 generic theorems about exponentials; general tidying up
2004-03-04 paulson 2004-03-04 new material from Avigad, and simplified treatment of division by 0
2004-03-01 paulson 2004-03-01 new Ring_and_Field hierarchy, eliminating redundant axioms
2004-02-15 paulson 2004-02-15 Polymorphic treatment of binary arithmetic using axclasses
2004-02-05 paulson 2004-02-05 tidying up, especially the Complex numbers
2004-02-03 paulson 2004-02-03 further tidying of the complex numbers
2004-02-03 paulson 2004-02-03 tidying of the complex numbers
2004-02-02 paulson 2004-02-02 Conversion of HyperNat to Isar format and its declaration as a semiring
2004-01-29 paulson 2004-01-29 simplifications in the hyperreals
2004-01-13 paulson 2004-01-13 types complex and hcomplex are now instances of class ringpower: omitting redundant lemmas
2004-01-06 paulson 2004-01-06 Ring_and_Field now requires axiom add_left_imp_eq for semirings. This allows more theorems to be proved for semirings, but requires a redundant axiom to be proved for rings, etc.
2004-01-03 paulson 2004-01-03 Deleting more redundant theorems
2004-01-01 paulson 2004-01-01 conversion of Real/PReal to Isar script; type "complex" is now in class "field"
2003-12-27 paulson 2003-12-27 re-organized numeric lemmas
2003-12-23 paulson 2003-12-23 converting Complex/Complex.ML to Isar
2003-12-23 paulson 2003-12-23 tidying up hcomplex arithmetic
2003-12-23 paulson 2003-12-23 type hcomplex is now in class field
2003-12-22 paulson 2003-12-22 converted Complex/NSComplex to Isar script
2003-05-05 paulson 2003-05-05 new session Complex for the complex numbers