diff --git a/README.hs b/README.hs
new file mode 100644
--- /dev/null
+++ b/README.hs
@@ -0,0 +1,70 @@
+-------------------------------------------------------------------------------
+-- | Constructive Algebra Library 
+-- 
+-- Anders Mortberg    <mortberg@student.chalmers.se>
+-- Bassel Mannaa      <mannaa@student.chalmers.se>
+--
+-- Abstract:
+-- This is a library written as part of our master theses. It focuses mainly
+-- on the theory of commutative rings from a constructive point of view. 
+--
+-------------------------------------------------------------------------------
+
+module README where
+
+
+--------------------------------------------------------------------------------
+-- Structures
+
+-- Rings with basic operations. 
+import Algebra.Structures.Ring
+
+-- Commutative rings.
+import Algebra.Structures.CommutativeRing
+
+-- Integral domains.
+import Algebra.Structures.IntegralDomain
+
+-- Fields.
+import Algebra.Structures.Field
+
+-- Strongly discrete rings - Rings with decidable ideal membership.
+import Algebra.Structures.StronglyDiscrete
+
+-- EuclideanDomains - Integral domains with decidable division and and Euclidean
+-- function. Contains lots of functions that are possible at the level of 
+-- Euclidean domain like the Euclidean algorithm and extended Euclidean 
+-- algorithm.
+import Algebra.Structures.EuclideanDomain
+
+-- Bezout domains - Non-Noetherian analogues of principal ideal domains. All 
+-- finitely generated ideals are principal.
+import Algebra.Structures.BezoutDomain
+
+-- GCD domains - Non-Noetherian analogues of unique factorization domains. 
+-- All pairs of nonzero elements have a greatest common divisor.
+import Algebra.Structures.GCDDomain
+
+-- Field of fractions of a GCD domain.
+import Algebra.Structures.FieldOfFractions
+
+
+-------------------------------------------------------------------------------
+-- Special constructions.
+
+-- Finitely generated ideals over commutative rings. 
+import Algebra.Ideal
+
+
+-------------------------------------------------------------------------------
+-- Instances.
+
+-- The integers.
+import Algebra.Z
+
+-- The rational numbers as the field of fractions of Z. 
+import Algebra.Q
+
+
+-------------------------------------------------------------------------------
+-- The end.
diff --git a/constructive-algebra.cabal b/constructive-algebra.cabal
--- a/constructive-algebra.cabal
+++ b/constructive-algebra.cabal
@@ -7,10 +7,19 @@
 -- The package version. See the Haskell package versioning policy
 -- (http://www.haskell.org/haskellwiki/Package_versioning_policy) for
 -- standards guiding when and how versions should be incremented.
-Version:             0.1
+Version:             0.1.1
 
 Synopsis:            A library of constructive algebra.
-Description:         A library of constructive algebra.
+Description:         
+        A library of algebra focusing mainly on commutative ring theory from a 
+        constructive point of view. 
+        .
+        Classical structures are implemented without Noetherian assumptions. 
+        This means that it is not assumed that all ideals are finitely 
+        generated. For example, instead of principal ideal domains one get 
+        Bezout domains which are integral domains in which all finitely 
+        generated ideals are principal (and not necessarily that all ideals are
+        principal).
 
 License:             BSD3
 License-file:        LICENSE
@@ -31,7 +40,7 @@
 
 -- Extra files to be distributed with the package, such as examples or
 -- a README.
--- Extra-source-files:  
+Extra-source-files:  README.hs, examples/Z_Examples.hs
 
 -- Constraint on the version of Cabal needed to build this package.
 Cabal-version:       >=1.2
@@ -43,11 +52,16 @@
                        Algebra.Structures.CommutativeRing,
                        Algebra.Structures.IntegralDomain, 
                        Algebra.Structures.Field,
+                       Algebra.Structures.BezoutDomain,
+                       Algebra.Structures.EuclideanDomain,
                        Algebra.Structures.StronglyDiscrete,
+                       Algebra.Structures.FieldOfFractions,
+                       Algebra.Structures.GCDDomain,         
                        Algebra.Ideal,
-                       Algebra.Z
+                       Algebra.Z,
+                       Algebra.Q
+                       
 
-  
   -- Packages needed in order to build this package.
   Build-depends:       base >= 3 && <= 4, QuickCheck >= 2 
   
diff --git a/examples/Z_Examples.hs b/examples/Z_Examples.hs
new file mode 100644
--- /dev/null
+++ b/examples/Z_Examples.hs
@@ -0,0 +1,27 @@
+module Z_Examples where
+
+import Test.QuickCheck
+
+import Algebra.Structures.BezoutDomain
+import Algebra.Structures.StronglyDiscrete
+import Algebra.Ideal
+import Algebra.Z
+
+
+-------------------------------------------------------------------------------
+-- Bezout domain examples
+
+ex1, ex2 :: (Ideal Z, [Z], [Z])
+ex1 = toPrincipal (Id [4,6])
+ex2 = toPrincipal (Id [2,3])
+
+ex3, ex4 :: Ideal Z
+ex3 = Id [2] `intersectionB` Id [3]
+ex4 = Id [2,3] `intersectionB` Id [3]
+
+
+-------------------------------------------------------------------------------
+-- Strong discreteness
+
+ex5 :: Maybe [Z]
+ex5 = member 2 ex3
diff --git a/src/Algebra/Ideal.hs b/src/Algebra/Ideal.hs
--- a/src/Algebra/Ideal.hs
+++ b/src/Algebra/Ideal.hs
@@ -1,7 +1,9 @@
 -- | Finitely generated ideals in commutative rings.
 module Algebra.Ideal
   ( Ideal(Id)
-  , zeroIdeal, isPrincipal, eval, addId, mulId 
+  , zeroIdeal, isPrincipal, fromId
+  , eval, addId, mulId
+  , isSameIdeal, zeroIdealWitnesses
   ) where
 
 import Data.List (intersperse,nub)
@@ -47,15 +49,18 @@
 mulId (Id xs) (Id ys) = if zs == [] then zeroIdeal else Id zs
   where zs = nub [ f <*> g | f <- xs, g <- ys, f <*> g /= zero ]
 
-{-| Test if an operations compute the correct ideal. 
+{- | Test if an operations compute the correct ideal. 
 The operation should give a witness that the comuted ideal contains
 the same elements.
 
-I `op` J = K
-[ x_1, ..., x_n ] `op` [ y_1, ..., y_m ] = [ z_1, ..., z_l ]
+If \[ x_1, ..., x_n \] \`op\` \[ y_1, ..., y_m \] = \[ z_1, ..., z_l \]
 
+Then the witness should give that
+
 z_k = a_k1 * x_1 + ... + a_kn * x_n
     = b_k1 * y_1 + ... + b_km * y_m
+
+This is used to check that the intersection computed is correct.
 
 -}
 isSameIdeal :: (CommutativeRing a, Eq a) 
diff --git a/src/Algebra/Q.hs b/src/Algebra/Q.hs
new file mode 100644
--- /dev/null
+++ b/src/Algebra/Q.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE TypeSynonymInstances #-}
+-- | Representation of rational numbers as the field of fractions of Z.
+module Algebra.Q 
+  ( Q
+  , toQ, toZ
+  ) where
+
+import Test.QuickCheck
+-- import qualified Math.Algebra.Field.Base as A (Q(..)) 
+-- import Data.Ratio 
+
+import Algebra.Structures.Field
+import Algebra.Structures.FieldOfFractions
+import Algebra.Z
+
+-------------------------------------------------------------------------------
+-- | Q is the field of fractions of Z.
+
+type Q = FieldOfFractions Z
+
+instance Num Q where
+  (+)              = (<+>)
+  (*)              = (<*>)
+  abs (F (a,b))    = F (abs a, b) 
+  signum (F (a,_)) = F (signum a,one)
+  fromInteger      = toQ
+
+instance Fractional Q where
+  (/) = (</>)
+  fromRational = undefined
+--   fromRational (a :% b) = reduce $ F (a,b)
+
+toQ :: Z -> Q
+toQ = toFieldOfFractions
+
+toZ :: Q -> Z
+toZ = fromFieldOfFractions   
diff --git a/src/Algebra/Structures/BezoutDomain.hs b/src/Algebra/Structures/BezoutDomain.hs
new file mode 100644
--- /dev/null
+++ b/src/Algebra/Structures/BezoutDomain.hs
@@ -0,0 +1,200 @@
+-- | Representation of Bezout domains. That is non-Noetherian analogues of 
+-- principal ideal domains. This means that all finitely generated ideals are
+-- principal.
+--
+{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
+module Algebra.Structures.BezoutDomain
+  ( BezoutDomain(..)
+  , propBezoutDomain
+  , intersectionB, intersectionBWitness
+  ) where
+
+import Test.QuickCheck 
+
+import Algebra.Structures.IntegralDomain
+-- import Algebra.Structures.Coherent
+import Algebra.Structures.EuclideanDomain
+-- import Algebra.Structures.PruferDomain
+import Algebra.Structures.StronglyDiscrete
+-- import Algebra.PLM
+-- import Algebra.Matrix
+import Algebra.Ideal
+
+
+-------------------------------------------------------------------------------
+-- | Bezout domains
+-- 
+-- Compute a principal ideal from another ideal. Also give witness that the
+-- principal ideal is equal to the first ideal.
+--
+-- toPrincipal \<a_1,...,a_n> = (\<a>,u_i,v_i)
+--   where
+--
+--   sum (u_i * a_i) = a
+--
+--   a_i = v_i * a
+--
+class IntegralDomain a => BezoutDomain a where
+  toPrincipal :: Ideal a -> (Ideal a,[a],[a])
+
+propToPrincipal :: (BezoutDomain a, Eq a) => Ideal a -> Bool
+propToPrincipal = isPrincipal . (\(a,_,_) -> a) . toPrincipal
+
+propIsSameIdeal :: (BezoutDomain a, Eq a) => Ideal a -> Bool
+propIsSameIdeal (Id as) =
+  let (Id [a], us, vs) = toPrincipal (Id as) 
+  in a == foldr1 (<+>) (zipWith (<*>) as us) 
+  && and [ ai == a <*> vi | (ai,vi) <- zip as vs ]
+  && length us == l_as && length vs == l_as
+  where l_as = length as
+
+propBezoutDomain :: (BezoutDomain a, Eq a) => Ideal a -> a -> a -> a -> Property
+propBezoutDomain id@(Id xs) a b c = zero `notElem` xs ==> 
+  if propToPrincipal id
+     then if propIsSameIdeal id
+             then propIntegralDomain a b c 
+             else whenFail (print "propIsSameIdeal") False
+     else whenFail (print "propToPrincipal") False
+
+
+-------------------------------------------------------------------------------
+-- Euclidean domain -> Bezout domain
+
+instance (EuclideanDomain a, Eq a) => BezoutDomain a where
+  toPrincipal (Id [x]) = (Id [x], [one], [one])
+  toPrincipal (Id xs)  = (Id [a], as, [ quotient ai a | ai <- xs ])
+    where
+    a  = genEuclidAlg xs
+    as = genExtendedEuclidAlg xs
+
+
+-------------------------------------------------------------------------------
+-- | Intersection of ideals with witness.
+-- 
+-- If one of the ideals is the zero ideal then the intersection is the zero 
+-- ideal.
+-- 
+intersectionBWitness :: (BezoutDomain a, Eq a) 
+              => Ideal a 
+              -> Ideal a 
+              -> (Ideal a, [[a]], [[a]])
+intersectionBWitness (Id xs) (Id ys) 
+  | xs' == [] = zeroIdealWitnesses xs ys
+  | ys' == [] = zeroIdealWitnesses xs ys
+  | otherwise = (Id [l], [handleZero xs as], [handleZero ys bs])
+  where
+  xs'            = filter (/= zero) xs
+  ys'            = filter (/= zero) ys
+
+  (Id [a],us1,vs1) = toPrincipal (Id xs') 
+  (Id [b],us2,vs2) = toPrincipal (Id ys')
+
+  (Id [g],[u1,u2],[v1,v2]) = toPrincipal (Id [a,b])
+
+  l  = g <*> v1 <*> v2
+  as = map (v2 <*>) us1
+  bs = map (v1 <*>) us2
+  
+  -- Handle the zeroes specially. If the first element in xs is a zero
+  -- then the witness should be zero otherwise use the computed witness. 
+  handleZero xs [] 
+    | all (==zero) xs = xs
+    | otherwise       = error "intersectionB: This should be impossible"
+  handleZero (x:xs) (a:as) 
+    | x == zero = zero : handleZero xs (a:as)
+    | otherwise = a    : handleZero xs as
+  handleZero [] _  = error "intersectionB: This should be impossible"
+
+
+-- | Intersection without witness.
+intersectionB :: (BezoutDomain a, Eq a) => Ideal a -> Ideal a -> Ideal a
+intersectionB a b = (\(x,_,_) -> x) $ intersectionBWitness a b
+
+
+-------------------------------------------------------------------------------
+-- Coherence
+-- 
+-- solveB :: (BezoutDomain a, Eq a) => Vector a -> Matrix a
+-- solveB x = solveWithIntersection x intersectionB
+
+-- instance (BezoutDomain r, Eq r) => Coherent r where
+--   solve x = solveWithIntersection x intersectionB
+
+
+-------------------------------------------------------------------------------
+-- Principal localization matrix
+--
+-- computePLM_B :: (BezoutDomain a, Eq a) => Ideal a -> Matrix a
+-- computePLM_B (Id xs) = 
+--  let (Id [g],us,ys) = toPrincipal (Id xs)
+--      n              = length xs - 1
+--  in M [ Vec [ us !! i <*> ys !! j | j <- [0..n] ] | i <- [0..n] ]
+
+
+-------------------------------------------------------------------------------
+-- | Strongly discreteness for Bezout domains
+-- 
+-- Given x, compute as such that x = sum (a_i * x_i)
+--
+instance (BezoutDomain a, Eq a) => StronglyDiscrete a where
+  member x (Id xs) | x == zero = Just (replicate (length xs) zero)
+                   | otherwise = if a == g 
+                                    then Just witness 
+                                    else Nothing
+    where
+    -- (<g>, as, bs)   = <x1,...,xn>
+    -- sum (a_i * x_i) = g
+    -- x_i             = b_i * g
+    (Id [g], as, bs) = toPrincipal (Id xs)
+    (Id [a], _,[q1,q2]) = toPrincipal (Id [x,g])
+    
+    -- x = qg = q (sum (ai * xi)) = sum (q * ai * xi)
+    witness = map (q1 <*>) as
+
+--------------------------------------------------------------------------------
+-- | Bezout domain -> Prüfer domain
+--
+{-
+Prufer: forall a b exists u v w t.  u+t = 1 &  ua = vb & wa = tb
+
+We consider only domain.
+We assume we have the Bezout condition: given a, b we can find g,a1,b1,c,d s.t.
+
+a = g a1
+b = g b1
+1 = c a1 + d b1
+
+We try then 
+
+u = d b1
+t = c a1
+
+We should find v such that
+a d b1 = b v
+this simplifies to 
+g a1 d b1 = g b1 v
+and we can take 
+v = a1 d
+Similarly we can take 
+w = b1 c
+
+We have shown that Bezout domain -> Prufer domain.
+instance (BezoutDomain a, Eq a) => PruferDomain a where
+  calcUVW a b | a == zero = (one,zero,zero)
+              | b == zero = (zero,zero,zero)
+              | otherwise = fromUVWTtoUVW (u,v,w,t)
+    where
+    -- Compute g, a1 and b1 such that:
+    -- a = g*a1
+    -- b = g*b1
+    (g,[_,_],[a1,b1])  = toPrincipal (Id [a,b])
+    
+    -- Compute c and d such that:
+    -- 1 = a1*c + a2*d
+    (_,[c,d],_) = toPrincipal (Id [a1,b1])
+
+    u = d <*> b1
+    t = c <*> a1
+    v = d <*> a1
+    w = c <*> b1
+-}
diff --git a/src/Algebra/Structures/CommutativeRing.hs b/src/Algebra/Structures/CommutativeRing.hs
--- a/src/Algebra/Structures/CommutativeRing.hs
+++ b/src/Algebra/Structures/CommutativeRing.hs
@@ -10,7 +10,7 @@
 
 
 -------------------------------------------------------------------------------
--- | Definition of commutative rings
+-- | Definition of commutative rings.
 
 class Ring a => CommutativeRing a
 
diff --git a/src/Algebra/Structures/EuclideanDomain.hs b/src/Algebra/Structures/EuclideanDomain.hs
new file mode 100644
--- /dev/null
+++ b/src/Algebra/Structures/EuclideanDomain.hs
@@ -0,0 +1,105 @@
+-- | Representation of Euclidean domains. That is integral domains with an 
+-- Euclidean functions and decidable division.
+--
+module Algebra.Structures.EuclideanDomain 
+  ( EuclideanDomain(..)
+  , propEuclideanDomain
+  , modulo, quotient, divides 
+  , euclidAlg, genEuclidAlg
+  , lcmE, genLcmE
+  , extendedEuclidAlg, genExtendedEuclidAlg
+  ) where
+
+import Test.QuickCheck
+
+import Algebra.Structures.IntegralDomain
+-- import Algebra.Structures.Coherent
+import Algebra.Ideal
+
+
+-------------------------------------------------------------------------------
+-- | Euclidean domains
+--
+-- Given a and b compute (q,r) such that a = bq + r and r = 0 || d r < d b. 
+-- Where d is the Euclidean function.
+
+class IntegralDomain a => EuclideanDomain a where
+  d :: a -> Integer
+  quotientRemainder :: a -> a -> (a,a)
+
+-- Check both that |a| <= |ab| and |a| >= 0 for all a,b
+propD :: (EuclideanDomain a, Eq a) => a -> a -> Bool
+propD a b = 
+  a == zero || b == zero || (d a <= d (a <*> b) && d a >= 0 && d b >= 0)
+
+propQuotRem :: (EuclideanDomain a, Eq a) => a -> a -> Bool
+propQuotRem a b = b == zero || (a == b <*> q <+> r && (r == zero || d r < d b))
+  where (q,r) = quotientRemainder a b 
+
+propEuclideanDomain :: (EuclideanDomain a, Eq a) => a -> a -> a -> Property
+propEuclideanDomain a b c =
+  if propD a b 
+     then if propQuotRem a b
+             then propIntegralDomain a b c
+             else whenFail (print "propQuotRem") False
+     else whenFail (print "propD") False
+
+
+-------------------------------------------------------------------------------
+-- Operations
+
+modulo :: EuclideanDomain a => a -> a -> a
+modulo a b = snd (quotientRemainder a b)
+
+quotient :: EuclideanDomain a => a -> a -> a
+quotient a b = fst (quotientRemainder a b)
+
+divides :: (EuclideanDomain a, Eq a) => a -> a -> Bool
+divides a b = modulo b a == zero
+
+-- | The Euclidean algorithm for calculating the GCD of a and b.
+euclidAlg :: (EuclideanDomain a, Eq a) => a -> a -> a
+euclidAlg a b | a == zero && b == zero = error "GCD of 0 and 0 is undefined"
+              | b == zero = a
+              | otherwise = euclidAlg b (a `modulo` b)
+
+-- | Generalized Euclidean algorithm to compute GCD of a list of elements.
+genEuclidAlg :: (EuclideanDomain a, Eq a) => [a] -> a
+genEuclidAlg = foldl euclidAlg zero
+
+-- | Lowest common multiple, (a*b)/gcd(a,b).
+lcmE :: (EuclideanDomain a, Eq a) => a -> a -> a
+lcmE a b = quotient (a <*> b) (euclidAlg a b)
+
+-- | Generalized lowest common multiple to compute lcm of a list of elements.
+genLcmE :: (EuclideanDomain a, Eq a) => [a] -> a
+genLcmE xs = quotient (foldr1 (<*>) xs) (genEuclidAlg xs)
+
+-- | The extended Euclidean algorithm. 
+-- 
+-- Computes x and y in ax + by = gcd(a,b).
+-- 
+extendedEuclidAlg :: (EuclideanDomain a, Eq a) => a -> a -> (a,a)
+extendedEuclidAlg a b | modulo a b == zero = (zero,one)
+                      | otherwise          = (y, x <-> y <*> (a `quotient` b))
+  where (x,y) = extendedEuclidAlg b (a `modulo` b)
+
+-- Specification of extended Euclidean algorithm.
+propExtendedEuclidAlg :: (EuclideanDomain a, Eq a) => a -> a -> Property
+propExtendedEuclidAlg a b = a /= zero && b /= zero ==> 
+  let (x,y) = extendedEuclidAlg a b in a <*> x <+> b <*> y == euclidAlg a b
+
+-- | Generalized extended Euclidean algorithm.
+--
+-- Solves a_1 x_1 + ... + a_n x_n = gcd (a_1,...,a_n)
+--
+genExtendedEuclidAlg :: (EuclideanDomain a, Eq a) => [a] -> [a]
+genExtendedEuclidAlg [x,y] = let (a,b) = extendedEuclidAlg x y in [a,b]
+genExtendedEuclidAlg xs    =
+  let (x,y) = extendedEuclidAlg (genEuclidAlg (init xs)) (last xs)
+  in map (x<*>) (genExtendedEuclidAlg (init xs)) ++ [y]
+
+-- Specification of generalized extended Euclidean algorithm. 
+propGenExtEuclidAlg :: (EuclideanDomain a, Eq a) => [a] -> Property
+propGenExtEuclidAlg xs = all (/= zero) xs && length xs >= 2 ==> 
+  foldr (<+>) zero (zipWith (<*>) (genExtendedEuclidAlg xs) xs) == genEuclidAlg xs
diff --git a/src/Algebra/Structures/Field.hs b/src/Algebra/Structures/Field.hs
--- a/src/Algebra/Structures/Field.hs
+++ b/src/Algebra/Structures/Field.hs
@@ -14,7 +14,7 @@
 infixl 7 </>
 
 -------------------------------------------------------------------------------
--- | Definition of fields
+-- | Definition of fields.
 
 class IntegralDomain a => Field a where
   inv :: a -> a
diff --git a/src/Algebra/Structures/FieldOfFractions.hs b/src/Algebra/Structures/FieldOfFractions.hs
new file mode 100644
--- /dev/null
+++ b/src/Algebra/Structures/FieldOfFractions.hs
@@ -0,0 +1,88 @@
+-- | The field of fractions over a GCD domain. The reason that it is an GCD 
+-- domain is that we only want to work over reduced quotients.
+module Algebra.Structures.FieldOfFractions
+  ( FieldOfFractions(..)
+  , toFieldOfFractions, fromFieldOfFractions
+  , reduce
+  ) where
+
+import Test.QuickCheck
+
+import Algebra.Structures.Field
+import Algebra.Structures.GCDDomain
+
+
+-------------------------------------------------------------------------------
+-- | Field of fractions
+
+newtype GCDDomain a => FieldOfFractions a = F (a,a)
+
+
+--------------------------------------------------------------------------------
+-- Instances
+
+instance (GCDDomain a, Show a, Eq a) => Show (FieldOfFractions a) where
+  show (F (a,b)) | b == one  = show a
+                 | otherwise = case show b of
+                    ('-':xs) -> "-" ++ show a ++ "/" ++ xs
+                    xs -> show a ++ "/" ++ xs
+
+instance (GCDDomain a, Eq a, Arbitrary a) => Arbitrary (FieldOfFractions a) where
+  arbitrary = do
+    a <- arbitrary
+    b <- arbitrary
+    if b == zero 
+       then return $ F (a,one)
+       else return $ F (a,b)
+
+instance (GCDDomain a, Eq a) => Eq (FieldOfFractions a) where
+  f == g = a <*> d == b <*> c
+    where
+    F (a,b) = reduce f
+    F (c,d) = reduce g
+
+instance (GCDDomain a, Eq a) => Ring (FieldOfFractions a) where
+  (F (a,b)) <+> (F (c,d)) = reduce (F (a <*> d <+> c <*> b,b <*> d))
+  (F (a,b)) <*> (F (c,d)) = reduce (F (a <*> c,b <*> d))
+  neg (F (a,b))           = reduce (F (neg a,b))
+  one                     = toFieldOfFractions one
+  zero                    = toFieldOfFractions zero
+
+instance (GCDDomain a, Eq a) => CommutativeRing (FieldOfFractions a)
+instance (GCDDomain a, Eq a) => IntegralDomain (FieldOfFractions a)
+
+instance (GCDDomain a, Eq a) => Field (FieldOfFractions a) where
+  inv (F (a,b)) | b /= zero && a /= zero = reduce $ F (b,a)
+                | otherwise = error "FieldOfFraction: Division by zero"
+
+
+--------------------------------------------------------------------------------
+-- Operations
+
+-- | Embed a value in the field of fractions.
+toFieldOfFractions :: GCDDomain a => a -> FieldOfFractions a
+toFieldOfFractions a = F (a,one)
+
+-- | Extract a value from the field of fractions. This is only possible if the
+-- divisor is one.
+fromFieldOfFractions :: (GCDDomain a, Eq a) => FieldOfFractions a -> a
+fromFieldOfFractions (F (a,b)) 
+  | b == one  = a
+  | otherwise = error "FieldOfFractions: Can't extract value"
+
+-- | Reduce an element.
+reduce :: (GCDDomain a, Eq a) => FieldOfFractions a -> FieldOfFractions a
+reduce (F (a,b)) | b == zero = error "FieldOfFractions: Division by zero"
+                 | a == zero = F (zero,one)
+                 | otherwise = if g == one
+                                  then F (a,b)
+                                  else F (x,y)
+  where
+  (g,x,y) = gcd' a b
+
+-- Specification of reduce.
+propReduce :: (GCDDomain a, Eq a) => FieldOfFractions a -> Property
+propReduce f@(F (a,b)) = a /= zero && b /= zero ==> g == one
+  where
+  F (c,d) = reduce f
+  (g,_,_) = gcd' c d
diff --git a/src/Algebra/Structures/GCDDomain.hs b/src/Algebra/Structures/GCDDomain.hs
new file mode 100644
--- /dev/null
+++ b/src/Algebra/Structures/GCDDomain.hs
@@ -0,0 +1,50 @@
+-- | Greatest common divisor (GCD) domains. 
+--
+-- GCD domains are integral domains in which every pair of nonzero elements 
+-- have a greatest common divisor. They can also be characterized as 
+-- non-Noetherian analogues of unique factorization domains.
+--
+{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
+module Algebra.Structures.GCDDomain 
+  ( GCDDomain(gcd')
+  , propGCDDomain
+  ) where
+
+import Test.QuickCheck
+
+import Algebra.Structures.IntegralDomain
+import Algebra.Structures.BezoutDomain
+import Algebra.Ideal
+
+
+-------------------------------------------------------------------------------
+-- | GCD domains
+
+class IntegralDomain a => GCDDomain a where
+  -- | Compute gcd(a,b) = (g,x,y) such that g = gcd(a,b) and
+  --   a = gx
+  --   b = gy
+  -- and a, b /= 0
+  gcd' :: a -> a -> (a,a,a)
+
+
+propGCD :: (GCDDomain a, Eq a) => a -> a -> Bool
+propGCD a b = a == zero || b == zero || a == g <*> x && b == g <*> y
+  where
+  (g,x,y) = gcd' a b
+
+
+-- | Specification of GCD domains. They are integral domains in which every 
+-- pair of nonzero elements have a greatest common divisor.
+propGCDDomain :: (Eq a, GCDDomain a, Arbitrary a, Show a) => a -> a -> a -> Property
+propGCDDomain a b c = if propGCD a b 
+                         then propIntegralDomain a b c
+                         else whenFail (print "propGCD") False
+
+-- This can be used to compute gcd of a list of non-zero elements
+-- genGCD :: ?
+-- genGCD = ?
+
+instance BezoutDomain a => GCDDomain a where
+  gcd' a b = (g,x,y)
+    where (Id [g],_,[x,y]) = toPrincipal (Id [a,b])
diff --git a/src/Algebra/Structures/IntegralDomain.hs b/src/Algebra/Structures/IntegralDomain.hs
--- a/src/Algebra/Structures/IntegralDomain.hs
+++ b/src/Algebra/Structures/IntegralDomain.hs
@@ -11,7 +11,7 @@
 
 
 -------------------------------------------------------------------------------
--- | Definition of integral domains
+-- | Definition of integral domains.
 
 class CommutativeRing a => IntegralDomain a
 
@@ -20,8 +20,8 @@
 propZeroDivisors a b = if a <*> b == zero then a == zero || b == zero else True
 
 
--- | Specification of commutative rings. Test that there are no zero-divisors
--- commutative and that it satisfies the axioms of commutative rings.
+-- | Specification of integral domains. Test that there are no zero-divisors
+-- and that it satisfies the axioms of commutative rings.
 propIntegralDomain :: (IntegralDomain a, Eq a) => a -> a -> a -> Property
 propIntegralDomain a b c = if propZeroDivisors a b
                               then propCommutativeRing a b c 
diff --git a/src/Algebra/Structures/Ring.hs b/src/Algebra/Structures/Ring.hs
--- a/src/Algebra/Structures/Ring.hs
+++ b/src/Algebra/Structures/Ring.hs
@@ -16,7 +16,7 @@
 
 
 -------------------------------------------------------------------------------
--- | Definition of rings
+-- | Definition of rings.
 
 class Ring a where
   -- | Addition
@@ -72,8 +72,7 @@
 propMulIdentity :: (Ring a, Eq a) => a -> (Bool,String)
 propMulIdentity a = (one <*> a == a && a <*> one == a, "propMulIdentity")
 
--- | Specification of rings.
--- Test that the arguments satisfy the ring axioms.
+-- | Specification of rings. Test that the arguments satisfy the ring axioms.
 propRing :: (Ring a, Eq a) => a -> a -> a -> Property
 propRing a b c = whenFail (print errorMsg) cond
   where
diff --git a/src/Algebra/Structures/StronglyDiscrete.hs b/src/Algebra/Structures/StronglyDiscrete.hs
--- a/src/Algebra/Structures/StronglyDiscrete.hs
+++ b/src/Algebra/Structures/StronglyDiscrete.hs
@@ -12,7 +12,7 @@
 --
 -- A ring is called strongly discrete if ideal membership is decidable.
 -- Nothing correspond to that x is not in the ideal and Just is the witness.
--- Examples include all euclidean domains and the polynomial ring.
+-- Examples include all Bezout domains and polynomial rings.
 --
 class Ring a => StronglyDiscrete a where
   member :: a -> Ideal a -> Maybe [a]
diff --git a/src/Algebra/Z.hs b/src/Algebra/Z.hs
--- a/src/Algebra/Z.hs
+++ b/src/Algebra/Z.hs
@@ -1,12 +1,16 @@
 {-# LANGUAGE TypeSynonymInstances #-}
 module Algebra.Z 
   ( Z
-  , module Algebra.Structures.IntegralDomain
+  , Ring(..)
   ) where
 
 import Test.QuickCheck
 
 import Algebra.Structures.IntegralDomain
+import Algebra.Structures.EuclideanDomain
+import Algebra.Structures.BezoutDomain
+import Algebra.Structures.StronglyDiscrete
+import Algebra.Ideal
 
 
 -- | Type synonym for integers.
@@ -25,3 +29,17 @@
 
 propIntegralDomainZ :: Z -> Z -> Z -> Property
 propIntegralDomainZ = propIntegralDomain
+
+instance EuclideanDomain Z where
+  d = abs
+  quotientRemainder = quotRem
+
+
+propEuclideanDomainZ :: Z -> Z -> Z -> Property
+propEuclideanDomainZ = propEuclideanDomain
+
+propBezoutDomainZ :: Ideal Z -> Z -> Z -> Z -> Property
+propBezoutDomainZ = propBezoutDomain
+
+propStronglyDiscreteZ :: Z -> Ideal Z -> Bool
+propStronglyDiscreteZ = propStronglyDiscrete