changeset 27487 | c8a6ce181805 |
parent 27368 | 9f90ac19e32b |
child 28952 | 15a4b2cf8c34 |
--- a/src/HOL/Library/Commutative_Ring.thy Fri Jul 04 16:33:08 2008 +0200 +++ b/src/HOL/Library/Commutative_Ring.thy Mon Jul 07 08:47:17 2008 +0200 @@ -7,7 +7,7 @@ header {* Proving equalities in commutative rings *} theory Commutative_Ring -imports Plain List Parity +imports Plain "~~/src/HOL/List" Parity uses ("comm_ring.ML") begin