content: /* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
   * Date: Wed Nov 26 11:26:00 CET 2014
   */
  package java.lang;
  
  public abstract class Enum extends java.lang.Object implements java.lang.Comparable, java.io.Serializable
  {
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.lang.String name();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final int ordinal();
  
     /*@ requires true; ensures true; assignable \everything; */
     protected Enum(java.lang.String arg0, int arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String toString();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final boolean equals(java.lang.Object arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final int hashCode();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.CloneNotSupportedException e) true; */
     protected final java.lang.Object clone() throws java.lang.CloneNotSupportedException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public final int compareTo(java.lang.Enum arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.lang.Class getDeclaringClass();
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.lang.Enum valueOf(java.lang.Class arg0, java.lang.String arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     protected final void finalize();
  
     /*@ requires true; ensures true; assignable \everything; */
     public int compareTo(java.lang.Object arg0);
  }
  