# HG changeset patch
# User haftmann
# Date 1265645544 -3600
# Node ID 1266f04f42ecf7372c4e2ecfc5b539d0100576bd
# Parent  a77d200e6503fbf3e2adf0934c810333ece02cea
tuned header

diff -r a77d200e6503 -r 1266f04f42ec src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Feb 08 17:12:22 2010 +0100
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Feb 08 17:12:24 2010 +0100
@@ -2,14 +2,13 @@
     Author:     Amine Chaieb
 *)
 
-header {* Implementation and verification of mutivariate polynomials Library *}
-
+header {* Implementation and verification of multivariate polynomials *}
 
 theory Reflected_Multivariate_Polynomial
-imports Parity Abstract_Rat Efficient_Nat List Polynomial_List
+imports Complex_Main Abstract_Rat Polynomial_List
 begin
 
-  (* Impelementation *)
+  (* Implementation *)
 
 subsection{* Datatype of polynomial expressions *}