--- a/src/HOL/Library/Commutative_Ring.thy Wed Dec 03 09:53:58 2008 +0100
+++ b/src/HOL/Library/Commutative_Ring.thy Wed Dec 03 15:58:44 2008 +0100
@@ -1,5 +1,4 @@
-(* ID: $Id$
- Author: Bernhard Haeupler
+(* Author: Bernhard Haeupler
Proving equalities in commutative rings done "right" in Isabelle/HOL.
*)
@@ -7,7 +6,7 @@
header {* Proving equalities in commutative rings *}
theory Commutative_Ring
-imports Plain "~~/src/HOL/List" Parity
+imports Plain "~~/src/HOL/List" "~~/src/HOL/Parity"
uses ("comm_ring.ML")
begin