| changeset 13339 | 0f89104dd377 |
| parent 12820 | 02e2ff3e4d37 |
| child 16417 | 9bc16273c2d4 |
--- a/src/ZF/AC/WO1_WO7.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/AC/WO1_WO7.thy Wed Jul 10 16:54:07 2002 +0200 @@ -52,7 +52,7 @@ apply (unfold wf_on_def wf_def) apply (drule nat_le_infinite_Ord [THEN le_imp_subset], assumption) apply (rule notI) -apply (erule_tac x = "nat" in allE, blast) +apply (erule_tac x = nat in allE, blast) done lemma converse_Memrel_not_well_ord: