| changeset 12814 | 2f5edb146f7e |
| parent 12788 | 6842f90972da |
| child 12820 | 02e2ff3e4d37 |
--- a/src/ZF/AC/AC15_WO6.thy Fri Jan 18 17:45:19 2002 +0100 +++ b/src/ZF/AC/AC15_WO6.thy Fri Jan 18 17:46:17 2002 +0100 @@ -269,7 +269,7 @@ apply (drule bspec, assumption) apply (elim conjE) apply (erule lemma_aux [THEN exE], assumption) -apply (simp add: the_element) +apply (simp add: the_equality) done theorem AC13_AC1: "AC13(1) ==> AC1"