# 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 \ 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