changeset 13704 | 854501b1e957 |
parent 13595 | 7e6cdcd113a2 |
child 13735 | 7de9342aca7a |
--- a/src/HOL/Finite_Set.thy Sat Nov 09 00:12:25 2002 +0100 +++ b/src/HOL/Finite_Set.thy Wed Nov 13 15:24:42 2002 +0100 @@ -304,7 +304,7 @@ apply (rule trancl_subset_Field2 [THEN finite_subset]) apply (rule finite_SigmaI) prefer 3 - apply (blast intro: r_into_trancl finite_subset) + apply (blast intro: r_into_trancl' finite_subset) apply (auto simp add: finite_Field) done