changeset 120 | 09287f26bfb8 |
parent 14 | 1c0926788772 |
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