# HG changeset patch
# User oheimb
# Date 893172167 -7200
# Node ID 8b81289852e394a29d670ac5a27c72c2dff1aeda
# Parent  64f075872f69f95538cd4be2efd9d6195ccc8e31
made proof of zmult_congruent2 more stable

diff -r 64f075872f69 -r 8b81289852e3 src/HOL/Integ/Integ.ML
--- a/src/HOL/Integ/Integ.ML	Tue Apr 21 17:22:03 1998 +0200
+++ b/src/HOL/Integ/Integ.ML	Tue Apr 21 17:22:47 1998 +0200
@@ -321,10 +321,11 @@
 \               split (%x1 y1. split (%x2 y2.   \
 \                   intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)";
 by (rtac (equiv_intrel RS congruent2_commuteI) 1);
+ by (pair_tac "w" 2);
+ by (rename_tac "z1 z2" 2);
  by Safe_tac;
  by (rewtac split_def);
  by (simp_tac (simpset() addsimps add_ac@mult_ac) 1);
-by (rename_tac "x1 y1 x2 y2 z1 z2" 1);
 by (asm_simp_tac (simpset() delsimps [equiv_intrel_iff]
                            addsimps add_ac@mult_ac) 1);
 by (rtac (intrelI RS(equiv_intrel RS equiv_class_eq)) 1);