changeset 25762 | c03e9d04b3e4 |
parent 25571 | c9e39eafc7a0 |
--- a/src/HOL/IntDef.thy Wed Jan 02 12:22:38 2008 +0100 +++ b/src/HOL/IntDef.thy Wed Jan 02 15:14:02 2008 +0100 @@ -22,7 +22,7 @@ int = "UNIV//intrel" by (auto simp add: quotient_def) -instantiation int :: "{zero, one, plus, minus, times, ord, abs, sgn}" +instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}" begin definition