# HG changeset patch
# User wenzelm
# Date 1128086224 -7200
# Node ID 25ffdae37db187c360e171866d23bd7f9ee280a9
# Parent  5b71bef7ad10711cae7576b5160877bd9d25d292
converted to Isar theory format;

diff -r 5b71bef7ad10 -r 25ffdae37db1 src/HOL/Algebra/poly/Polynomial.thy
--- a/src/HOL/Algebra/poly/Polynomial.thy	Fri Sep 30 13:47:36 2005 +0200
+++ b/src/HOL/Algebra/poly/Polynomial.thy	Fri Sep 30 15:17:04 2005 +0200
@@ -4,8 +4,8 @@
     Author: Clemens Ballarin, started 17 July 1997
 *)
 
-Polynomial = LongDiv
-
+theory Polynomial
+imports LongDiv
+begin
 
-
-
+end