| changeset 120 | 09287f26bfb8 |
| parent 15 | 6c6d2f6e3185 |
| child 129 | dc50a4b96d7b |
--- a/src/ZF/QUniv.ML Mon Nov 15 14:33:40 1993 +0100 +++ b/src/ZF/QUniv.ML Mon Nov 15 14:41:25 1993 +0100 @@ -290,7 +290,7 @@ val QPair_Int_Vfrom_in_quniv = result(); -(**** "Take-lemma" rules for proving a=b by co-induction ****) +(**** "Take-lemma" rules for proving a=b by coinduction ****) (** Unfortunately, the technique used above does not apply here, since the base case appears impossible to prove: it involves an intersection