src/HOL/Hyperreal/NthRoot.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-05-21 wenzelm 2004-05-21 tuned document;
2004-03-19 paulson 2004-03-19 conversion of Hyperreal/Lim to new-style
2004-01-27 paulson 2004-01-27 replacing HOL/Real/PRat, PNat by the rational number development of Markus Wenzel
2004-01-14 nipkow 2004-01-14 Told linear arithmetic package about injections "real" from nat/int into real.
2004-01-09 paulson 2004-01-09 Defining the type class "ringpower" and deleting superseded theorems for types nat, int, real, hypreal
2004-01-01 paulson 2004-01-01 tweaking of lemmas in RealDef, RealOrd
2003-12-23 paulson 2003-12-23 removing real_of_posnat
2003-12-23 paulson 2003-12-23 converting Hyperreal/NthRoot to Isar
2003-11-27 paulson 2003-11-27 Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files. New theorems for Ring_and_Field. Fixing affected proofs.
2001-11-15 paulson 2001-11-15 new theories from Jacques Fleuriot