00001: public class ExpInt extends Exp
00002: {
00003:   public final int value;
00004: 
00005: 
00006:   public ExpInt (int value)
00007:   {
00008:     this.value = value;
00009:   }
00010: 
00011: 
00012:   public String toString ()
00013:   {
00014:     return Integer.toString (value);
00015:   }
00016: }
00017: