src/HOL/Algebra/abstract/PID.thy

--- a/src/HOL/Algebra/abstract/PID.thy	Thu Aug 03 14:53:57 2006 +0200
+++ b/src/HOL/Algebra/abstract/PID.thy	Thu Aug 03 14:57:26 2006 +0200
@@ -4,7 +4,7 @@
     Author: Clemens Ballarin, started 5 October 1999
 *)
 
-theory PID imports Ideal begin
+theory PID imports Ideal2 begin
 
 instance pid < factorial
   apply intro_classes