//  This code is inserted into the SpecJava class
//  directly.  It comes from the <project>.include.java
//  file in the current directory.  It can be editted either
//  with your favorite text editor, or via the "edit code"
//  option of the edit menu.