# HG changeset patch
# User haftmann
# Date 1239802440 -7200
# Node ID 3a30613aa469f1982e35b32a97b3500186b42533
# Parent  c38cbc0ac8d15043551814dd0105b6c9a81da3f4
index type is a semiring_div

diff -r c38cbc0ac8d1 -r 3a30613aa469 src/HOL/Library/Code_Index.thy
--- a/src/HOL/Library/Code_Index.thy	Wed Apr 15 15:30:39 2009 +0200
+++ b/src/HOL/Library/Code_Index.thy	Wed Apr 15 15:34:00 2009 +0200
@@ -144,7 +144,7 @@
 
 subsection {* Basic arithmetic *}
 
-instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}"
+instantiation index :: "{minus, ordered_semidom, semiring_div, linorder}"
 begin
 
 definition [simp, code del]:
@@ -172,7 +172,7 @@
   "n < m \<longleftrightarrow> nat_of n < nat_of m"
 
 instance proof
-qed (auto simp add: left_distrib)
+qed (auto simp add: index left_distrib div_mult_self1)
 
 end