src/HOL/Integ/Integ.ML
changeset 5278 a903b66822e2
parent 5184 9b8547a9496a
child 5316 7a8975451a89
     1.1 --- a/src/HOL/Integ/Integ.ML	Thu Aug 06 15:47:26 1998 +0200
     1.2 +++ b/src/HOL/Integ/Integ.ML	Thu Aug 06 15:48:13 1998 +0200
     1.3 @@ -316,8 +316,7 @@
     1.4  by (simp_tac (simpset() addsimps add_ac) 1);
     1.5  qed "zmult_congruent_lemma";
     1.6  
     1.7 -Goal 
     1.8 -    "congruent2 intrel (%p1 p2.                 \
     1.9 +Goal "congruent2 intrel (%p1 p2.                 \
    1.10  \               split (%x1 y1. split (%x2 y2.   \
    1.11  \                   intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)";
    1.12  by (rtac (equiv_intrel RS congruent2_commuteI) 1);