src/HOL/Decision_Procs/Commutative_Ring.thy
changeset 58770 ae5e9b4f8daf
parent 58712 709d8f68ec29
child 58834 773b378d9313
     1.1 --- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Thu Oct 23 14:04:05 2014 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Thu Oct 23 14:04:05 2014 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Proving equalities in commutative rings *}
     1.5  
     1.6  theory Commutative_Ring
     1.7 -imports Parity
     1.8 +imports Main
     1.9  begin
    1.10  
    1.11  text {* Syntax of multivariate polynomials (pol) and polynomial expressions. *}