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