author | paulson |
Thu, 27 Nov 2003 10:47:55 +0100 | |
changeset 14268 | 5cf13e80be0e |
parent 12196 | a3be6b3a9c0b |
child 14324 | c9c6832f9b22 |
permissions | -rw-r--r-- |
12196 | 1 |
(* Title : NthRoot.thy |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 1998 University of Cambridge |
|
4 |
Description : Existence of nth root. Adapted from |
|
5 |
http://www.math.unl.edu/~webnotes |
|
6 |
*) |
|
7 |
||
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
12196
diff
changeset
|
8 |
NthRoot = SEQ + HSeries |