src/HOL/Algebra/IntRing.thy
changeset 25919 8b1c0d434824
parent 24131 1099f6c73649
child 27713 95b36bfe7fc4
equal deleted inserted replaced
25918:82dd239e0f65 25919:8b1c0d434824
     3   Id:        $Id$
     3   Id:        $Id$
     4   Author:    Stephan Hohe, TU Muenchen
     4   Author:    Stephan Hohe, TU Muenchen
     5 *)
     5 *)
     6 
     6 
     7 theory IntRing
     7 theory IntRing
     8 imports QuotRing IntDef
     8 imports QuotRing Int
     9 begin
     9 begin
    10 
    10 
    11 
    11 
    12 section {* The Ring of Integers *}
    12 section {* The Ring of Integers *}
    13 
    13