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