src/HOL/Finite.ML
changeset 1782 ab45b881fa62
parent 1760 6f41a494f3b1
child 1786 8a31d85d27b8
     1.1 --- a/src/HOL/Finite.ML	Fri May 31 20:25:59 1996 +0200
     1.2 +++ b/src/HOL/Finite.ML	Mon Jun 03 11:41:00 1996 +0200
     1.3 @@ -201,9 +201,7 @@
     1.4  by (etac exE 1);
     1.5  by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
     1.6  by (rtac exI 1);
     1.7 -by (rtac conjI 1);
     1.8 - br disjI2 1;
     1.9 - br refl 1;
    1.10 +by (rtac (refl RS disjI2 RS conjI) 1);
    1.11  by (etac equalityE 1);
    1.12  by (asm_full_simp_tac
    1.13       (!simpset addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1);