changeset 13175 | 81082cfa5618 |
parent 13174 | 85d3c0981a16 |
child 13244 | 7b37e218f298 |
--- a/src/ZF/OrdQuant.thy Wed May 22 19:34:01 2002 +0200 +++ b/src/ZF/OrdQuant.thy Thu May 23 17:05:21 2002 +0200 @@ -182,8 +182,6 @@ "[| i=j; !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))" by (simp add: OUnion_def lt_def OUN_iff) -declare ltD [THEN beta, simp] - lemma lt_induct: "[| i<k; !!x.[| x<k; ALL y<x. P(y) |] ==> P(x) |] ==> P(i)" apply (simp add: lt_def oall_def)