body { background-color: #ccf; line-height: 160% }
/*h1 { line-height: 60% }*/
h1 { margin: 10px 0px 2px 0px; color: blue; font-size: 120%; }
h2 { margin: 10px 0px 4px 0px; color: blue; font-size: 100%; }
.fn { color: brown; border-radius: 3px;
      background-color: white; padding: 0px 4px;
      margin: 0px 3px; }
/*.str { color: blue; }*/
.ex { border: 0px solid #aaa; padding: 2px 4px 2px 4px;
      margin: 0px 2px; border-radius: 3px;
      white-space: nowrap;
      background-color: #eef;
      }
/*.fn { font-family: monospace; }*/
/*
.ans { border: 1px solid #eee; padding: 0px 3px;
        border-radius: 3px; background-color: #eee;
        display: none; }
.ans { background-color: #abc }*/