changeset 12196 | a3be6b3a9c0b |
child 14268 | 5cf13e80be0e |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hyperreal/NthRoot.thy Thu Nov 15 16:12:49 2001 +0100 @@ -0,0 +1,8 @@ +(* Title : NthRoot.thy + Author : Jacques D. Fleuriot + Copyright : 1998 University of Cambridge + Description : Existence of nth root. Adapted from + http://www.math.unl.edu/~webnotes +*) + +NthRoot = SEQ + ExtraThms2