| changeset 5516 | d80e9aeb4a2b |
| parent 5477 | 41ab0f44dd8f |
| child 5537 | c2bd39a2c0ee |
--- a/src/HOL/Finite.ML Mon Sep 21 12:01:14 1998 +0200 +++ b/src/HOL/Finite.ML Mon Sep 21 15:58:27 1998 +0200 @@ -187,8 +187,8 @@ by (etac finite_imageI 1); by (simp_tac (simpset() addsimps [converse_def,image_def]) 1); by Auto_tac; - by (rtac bexI 1); - by (assume_tac 2); +by (rtac bexI 1); +by (assume_tac 2); by (Simp_tac 1); qed "finite_converse"; AddIffs [finite_converse];