renamed vars in zle_trans for compatibility
authornipkow
Sun Jun 17 08:56:13 2007 +0200 (2007-06-17)
changeset 234026472c689664f
parent 23401 8c5532263ba9
child 23403 9e1edc15ef52
renamed vars in zle_trans for compatibility
src/HOL/IntDef.thy
     1.1 --- a/src/HOL/IntDef.thy	Sat Jun 16 16:27:35 2007 +0200
     1.2 +++ b/src/HOL/IntDef.thy	Sun Jun 17 08:56:13 2007 +0200
     1.3 @@ -739,7 +739,7 @@
     1.4  lemmas zmult_1_right = mult_1_right [where 'a=int]
     1.5  
     1.6  lemmas zle_refl = order_refl [where 'a=int]
     1.7 -lemmas zle_trans = order_trans [where 'a=int]
     1.8 +lemmas zle_trans = order_trans [where 'a=int and x="?i" and y="?j" and z="?k"]
     1.9  lemmas zle_anti_sym = order_antisym [where 'a=int]
    1.10  lemmas zle_linear = linorder_linear [where 'a=int]
    1.11  lemmas zless_linear = linorder_less_linear [where 'a = int]