diff -r 85d3c0981a16 -r 81082cfa5618 src/ZF/OrdQuant.thy
--- 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)