1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
\contentsline {chapter}{\numberline {1}Statement of Rights}{3}
\contentsline {chapter}{\numberline {2}The window Library}{5}
\contentsline {section}{\numberline {2.1}Window Inference}{5}
\contentsline {section}{\numberline {2.2}Getting Started}{6}
\contentsline {section}{\numberline {2.3}Transforming the Focus}{7}
\contentsline {section}{\numberline {2.4}Opening subwindows}{8}
\contentsline {section}{\numberline {2.5}Lemmas}{10}
\contentsline {subsection}{\numberline {2.5.1}Windows on the Context}{11}
\contentsline {section}{\numberline {2.6}Conjectures}{12}
\contentsline {section}{\numberline {2.7}Window Stacks}{14}
\contentsline {subsection}{\numberline {2.7.1}The xlabel Library Component}{15}
\contentsline {section}{\numberline {2.8}Batch Proof}{15}
\contentsline {section}{\numberline {2.9}The tactic Library Component}{16}
\contentsline {section}{\numberline {2.10}Adding New Window Rules}{18}
\contentsline {section}{\numberline {2.11}Adding New Relations}{20}
\contentsline {subsection}{\numberline {2.11.1}Relative Strengths}{21}
\contentsline {section}{\numberline {2.12}Future Changes}{22}
\contentsline {section}{\numberline {2.13}Bugs}{22}
\contentsline {chapter}{\numberline {3}ML Functions in the window Library}{25}
\contentsline {chapter}{\numberline {4}Pre-proved Theorems}{95}
\contentsline {section}{\numberline {4.1}Definitions}{95}
\contentsline {section}{\numberline {4.2}Theorems}{95}
\contentsline {chapter}{Index}{96}
|
