equal
deleted
inserted
replaced
288 by (rtac (QPair_in_quniv RS qunivD) 2); |
288 by (rtac (QPair_in_quniv RS qunivD) 2); |
289 by (REPEAT (assume_tac 1)); |
289 by (REPEAT (assume_tac 1)); |
290 val QPair_Int_Vfrom_in_quniv = result(); |
290 val QPair_Int_Vfrom_in_quniv = result(); |
291 |
291 |
292 |
292 |
293 (**** "Take-lemma" rules for proving a=b by co-induction ****) |
293 (**** "Take-lemma" rules for proving a=b by coinduction ****) |
294 |
294 |
295 (** Unfortunately, the technique used above does not apply here, since |
295 (** Unfortunately, the technique used above does not apply here, since |
296 the base case appears impossible to prove: it involves an intersection |
296 the base case appears impossible to prove: it involves an intersection |
297 with eclose(X) for arbitrary X. So a=b is proved by transfinite induction |
297 with eclose(X) for arbitrary X. So a=b is proved by transfinite induction |
298 over ALL ordinals, using Vset(i) instead of Vfrom(X,i). |
298 over ALL ordinals, using Vset(i) instead of Vfrom(X,i). |