/* doc.css for documents
   last modified. 2005.10.21
   ver.             01.02.02
*/

body {
  width:840px;
  margin:10px auto 15px;

  padding:0px;
}


#main {
  padding:10px;

  border:1px solid #00ff00;
}


h5 {
  margin-top: 0px;

  text-align: right;
}

.title {
  margin-bottom: 10px;
  margin-left: 24px;
}


a {
  margin-right: 2px;
  margin-left: 10px;
}


/** pre **/
.file {
  font-family: "Times New Roman", "Times", "serif";

  border:1px solid #000000;
}

.console {
  font-family: "Courier", "monospace";
  font-size: 8pt;

  border:1px solid #000000;
}

.input {
  color: #ff0000;
  font-weight: bold;
}