src/HOL/Hyperreal/NthRoot.thy
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