
diff -r 8c5532263ba9 -r 6472c689664f src/HOL/IntDef.thy
--- a/src/HOL/IntDef.thy	Sat Jun 16 16:27:35 2007 +0200
+++ b/src/HOL/IntDef.thy	Sun Jun 17 08:56:13 2007 +0200
@@ -739,7 +739,7 @@
 lemmas zmult_1_right = mult_1_right [where 'a=int]
 
 lemmas zle_refl = order_refl [where 'a=int]
-lemmas zle_trans = order_trans [where 'a=int]
+lemmas zle_trans = order_trans [where 'a=int and x="?i" and y="?j" and z="?k"]
 lemmas zle_anti_sym = order_antisym [where 'a=int]
 lemmas zle_linear = linorder_linear [where 'a=int]
 lemmas zless_linear = linorder_less_linear [where 'a = int]




