--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/poly/Degree.thy	Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,15 @@
+(*
+    Degree of polynomials
+    $Id$
+    written by Clemens Ballarin, started 22. 1. 1997
+*)
+
+Degree = PolyRing +
+
+consts
+  deg		:: ('a::ringS) up => nat
+
+defs
+  deg_def	"deg p == LEAST n. bound n (Rep_UP p)"
+
+end