/* font-family */
body {
	 font-family: Georgia, "DejaVu Serif", Times, "Times New Roman", serif;
}

h1, h2, h3, h4, h5, h6, 
div#nav, div#share, div#address {
	 font-family: Corbel, "Lucida Grande", "Lucida Sans Unicode", "Lucida Sans", "DejaVu Sans", 
	 "Bitstream Vera Sans", "Liberation Sans", Verdana, "Verdana Ref", sans-serif;
}

code, tt, pre { 
	 font-family: Consolas, "Andale Mono WT", "Andale Mono", "Lucida Console", 
	 "Lucida Sans Typewriter", "DejaVu Sans Mono", "Bitstream Vera Sans Mono", "Liberation Mono", 
	 "Nimbus Mono L", Monaco, "Courier New", Courier, monospace; 
}

/* font-size */
body {
	 font-size: 95%; 
	 line-height: 1.5; /* We can use unitless numbers here; they act as multiples of the font-size. */
}

div#header>h1 {
	 font-size: 4.25em;
}

div#nav, div#share {
	 font-size: 85%;
}

h1              { font-size: 2em;   line-height: 1.25; }
h2              { font-size: 1.4em; line-height: 1.25; }
h3, div.post h2, div.paper h2 { font-size: 1.2em; line-height: 1.25; }
h4, div.post h3, div.paper h3 { font-size: 1em;   line-height: 1.25; }

h5, div.post h4 { text-transform: uppercase; letter-spacing: 1px; }

span#tag { 	 font-size: 80%; }

pre {
	 font-size: 85%;
}





a {
	 text-decoration: none;
}

li {
	 line-height: 1.25;
}

h1 {
	 font-weight: bold;
	 font-style: normal;
}

span.title {
	 font-style: italic;
}