# HG changeset patch
# User nipkow
# Date 1182063373 -7200
# Node ID 6472c689664f92492bfa843bc40431799f91c7fe
# Parent  8c5532263ba9ca6ea0310a9cb004a25208f7d392
renamed vars in zle_trans for compatibility

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]