1.1 --- a/src/HOL/Library/Saturated.thy	Thu Sep 08 18:47:23 2011 -0700
     1.2 +++ b/src/HOL/Library/Saturated.thy	Thu Sep 08 19:35:23 2011 -0700
     1.3 @@ -63,7 +63,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -instantiation sat :: (len) "{minus, comm_semiring_0, comm_semiring_1}"
     1.8 +instantiation sat :: (len) "{minus, comm_semiring_1}"
     1.9  begin
    1.10  
    1.11  definition
    1.12 @@ -145,13 +145,17 @@
    1.13  
    1.14  end
    1.15  
    1.16 -instantiation sat :: (len) number
    1.17 +lemma Sat_eq_of_nat: "Sat n = of_nat n"
    1.18 +  by (rule sat_eqI, induct n, simp_all)
    1.19 +
    1.20 +instantiation sat :: (len) number_semiring
    1.21  begin
    1.22  
    1.23  definition
    1.24    number_of_sat_def [code del]: "number_of = Sat \<circ> nat"
    1.25  
    1.26 -instance ..
    1.27 +instance
    1.28 +  by default (simp add: number_of_sat_def Sat_eq_of_nat)
    1.29  
    1.30  end
    1.31