# HG changeset patch
# User huffman
# Date 1315535723 25200
# Node ID 41fddafe20d59c9c951428ba6be975966be59dee
# Parent  f4d0b060c7ca274635707b9837d5a15f12d6b82c
Library/Saturated.thy: number_semiring class instance

diff -r f4d0b060c7ca -r 41fddafe20d5 src/HOL/Library/Saturated.thy
--- a/src/HOL/Library/Saturated.thy	Thu Sep 08 18:47:23 2011 -0700
+++ b/src/HOL/Library/Saturated.thy	Thu Sep 08 19:35:23 2011 -0700
@@ -63,7 +63,7 @@
 
 end
 
-instantiation sat :: (len) "{minus, comm_semiring_0, comm_semiring_1}"
+instantiation sat :: (len) "{minus, comm_semiring_1}"
 begin
 
 definition
@@ -145,13 +145,17 @@
 
 end
 
-instantiation sat :: (len) number
+lemma Sat_eq_of_nat: "Sat n = of_nat n"
+  by (rule sat_eqI, induct n, simp_all)
+
+instantiation sat :: (len) number_semiring
 begin
 
 definition
   number_of_sat_def [code del]: "number_of = Sat \<circ> nat"
 
-instance ..
+instance
+  by default (simp add: number_of_sat_def Sat_eq_of_nat)
 
 end