src/HOL/Integ/IntDef.ML
changeset 9366 a83f3abbfc93
parent 9108 9fff97d29837
child 9392 c8e6529cc082
     1.1 --- a/src/HOL/Integ/IntDef.ML	Sun Jul 16 20:55:56 2000 +0200
     1.2 +++ b/src/HOL/Integ/IntDef.ML	Sun Jul 16 20:56:14 2000 +0200
     1.3 @@ -52,7 +52,9 @@
     1.4  qed "intrel_iff";
     1.5  
     1.6  Goal "(x,x): intrel";
     1.7 -by (stac surjective_pairing 1 THEN rtac (refl RS intrelI) 1);
     1.8 +by (pair_tac "x" 1);
     1.9 +by (rtac intrelI 1);
    1.10 +by (rtac refl 1);
    1.11  qed "intrel_refl";
    1.12  
    1.13  Goalw [equiv_def, refl_def, sym_def, trans_def]