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