--- a/src/HOL/Finite.ML Mon Mar 16 16:47:57 1998 +0100
+++ b/src/HOL/Finite.ML Mon Mar 16 16:50:50 1998 +0100
@@ -191,15 +191,15 @@
by (etac (rewrite_rule [inj_onto_def] finite_imageD) 1);
by (simp_tac (simpset() addsplits [expand_split]) 1);
by (etac finite_imageI 1);
-by (simp_tac (simpset() addsimps [inverse_def,image_def]) 1);
+by (simp_tac (simpset() addsimps [converse_def,image_def]) 1);
by Auto_tac;
by (rtac bexI 1);
by (assume_tac 2);
by (Simp_tac 1);
by (split_all_tac 1);
by (Asm_full_simp_tac 1);
-qed "finite_inverse";
-AddIffs [finite_inverse];
+qed "finite_converse";
+AddIffs [finite_converse];
section "Finite cardinality -- 'card'";