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