1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
pre.smallexample,
div.important,
div.note,
div.tip {background-color:rgb(240,240,240);
margin: 0px 40px 0px 40px;
border-width: 1px 2px 2px 1px;
border-top-style: ridge;
border-left-style: ridge;
border-right-style: solid;
border-bottom-style: solid;
border-color: black;}
pre.smallexample {font-size: 14px;
font-family: courier new,courier,fixed;
}
div.important,
div.note,
div.tip {font-size: 14px;
background-repeat: no-repeat;
background-position: center left;
padding: 10px 10px 10px 40px;
}
div.tip {background-image: url(tip.png); }
div.note {background-image: url(note.png); }
div.important {background-image: url(important.png); }
div.side {position: absolute;
font-style: italic;
font-size: small;
text-align: left;
width: 200px;
left: 840px;
z-index: 3;
color: #447bcd;}
div.side a:link,
div.side a:visited { text-decoration: none; color: #447bcd;}
div.contents ul ul { padding-left: 10px;
list-style-type: none;
}
div.contents > ul { padding-left: 5px;
list-style-type: none }
div.contents a:link,
div.contents a:visited,
div.contents a:active { text-decoration: none; color:blue }
div.contents a:hover { text-decoration: underline; color:red}
/* IE7 still does not support the > selectors... workaround */
div.contents ul li { padding-top: 20px; }
div.contents ul li ul li { padding-top: 0px; }
h1.settitle {background:#003580;
font-size: huge;
text-align: center;
padding: 30px 10px 30px 10px;
color: white }
h2.unnumbered,
h2.chapter { background:#098ABA;
padding: 5px 5px 5px 15px }
h3.section { border-bottom: solid black; }
h4.subsection { border-bottom: solid black;}
dt { text-decoration: underline;
font-style: italic }
code {color:black;
font-family: courier new,courier,fixed;
font-size: 14px;}
body {/*font-family: verdana,arial,helvetica,sans-serif;
font-size: 14px; */
margin-left:10px; margin-right:305px;
text-align: justify}
samp {font-family: courier new,courier,fixed;
font-size: 14px}
/* table of contents and tips in the right margin */
div.contents {width:300px; top: 0px; right:0px; font-size:smaller;
position: absolute; }
div.contents ul {padding-left:10px; margin:0}
div.tip {position: absolute;
text-align: left; /* don't align when width is small */
width: 200px; right:0px}
|
