Fix double declaration of method String#length in javaRedux: String.java

Author: unp1

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/String.java

@@ -4,12 +4,6 @@ public final class String extends java.lang.Object implements java.io.Serializab
 {
    // public final static java.util.Comparator CASE_INSENSITIVE_ORDER;
 
-   /*@ normal_behavior
-       ensures \result == \dl_seqLen(\dl_strContent(this));
-    */
-   public /*@pure*/ int length();
-
-
    /*@
    public normal_behavior
       requires true;