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
|
\relax
\@writefile{toc}{\string\contentsline\space {chapter}{\string\numberline\space {10}Theories}{115}}
\@writefile{lof}{\string\addvspace\space {10\p@ }}
\@writefile{lot}{\string\addvspace\space {10\p@ }}
\newlabel{semantics}{{10}{115}}
\@writefile{toc}{\string\contentsline\space {section}{\string\numberline\space {10.1}Introduction}{115}}
\@writefile{toc}{\string\contentsline\space {section}{\string\numberline\space {10.2}Sequents}{116}}
\newlabel{sequents}{{10.2}{116}}
\@writefile{toc}{\string\contentsline\space {section}{\string\numberline\space {10.3}Logic}{117}}
\@writefile{toc}{\string\contentsline\space {subsection}{\string\numberline\space {10.3.1}The HOL deductive system}{117}}
\newlabel{HOLrules}{{10.3.1}{117}}
\@writefile{toc}{\string\contentsline\space {subsection}{\string\numberline\space {10.3.2}Soundness theorem}{119}}
\newlabel{soundness}{{10.3.2}{119}}
\@writefile{toc}{\string\contentsline\space {section}{\string\numberline\space {10.4}HOL Theories}{120}}
\newlabel{theories}{{10.4}{120}}
\@writefile{toc}{\string\contentsline\space {subsection}{\string\numberline\space {10.4.1}The theory {\string\ptt\space MIN}}{120}}
\newlabel{min}{{10.4.1}{120}}
\@writefile{toc}{\string\contentsline\space {subsection}{\string\numberline\space {10.4.2}The theory {\string\ptt\space LOG}}{121}}
\newlabel{LOG}{{10.4.2}{121}}
\@writefile{toc}{\string\contentsline\space {subsection}{\string\numberline\space {10.4.3}The theory {\string\ptt\space INIT}}{123}}
\newlabel{INIT}{{10.4.3}{123}}
\@writefile{toc}{\string\contentsline\space {subsection}{\string\numberline\space {10.4.4}Consistency}{124}}
\newlabel{consistency}{{10.4.4}{124}}
\@writefile{toc}{\string\contentsline\space {section}{\string\numberline\space {10.5}Extensions of theories}{124}}
\newlabel{extensions}{{10.5}{124}}
\citation{Z}
\@writefile{toc}{\string\contentsline\space {subsection}{\string\numberline\space {10.5.1}Extension by constant definition}{125}}
\newlabel{defs}{{10.5.1}{125}}
\@writefile{toc}{\string\contentsline\space {subsection}{\string\numberline\space {10.5.2}Extension by constant specification}{127}}
\newlabel{specs}{{10.5.2}{127}}
\@writefile{toc}{\string\contentsline\space {subsection}{\string\numberline\space {10.5.3}Remarks about constants in HOL}{129}}
\newlabel{constants}{{10.5.3}{129}}
\@writefile{toc}{\string\contentsline\space {subsection}{\string\numberline\space {10.5.4}Extension by type definition}{130}}
\newlabel{tydefs}{{10.5.4}{130}}
\@writefile{toc}{\string\contentsline\space {subsection}{\string\numberline\space {10.5.5}Extension by type specification\string\footnotemark\space }{132}}
\newlabel{tyspecs}{{10.5.5}{132}}
\global\@namedef{cp@semantics}{
\setcounter{page}{137}
\setcounter{equation}{0}
\setcounter{enumi}{4}
\setcounter{enumii}{2}
\setcounter{enumiii}{2}
\setcounter{enumiv}{0}
\setcounter{footnote}{9}
\setcounter{mpfootnote}{0}
\setcounter{part}{2}
\setcounter{chapter}{10}
\setcounter{section}{5}
\setcounter{subsection}{5}
\setcounter{subsubsection}{0}
\setcounter{paragraph}{0}
\setcounter{subparagraph}{0}
\setcounter{figure}{0}
\setcounter{table}{0}
\setcounter{myenumi}{7}
\setcounter{sessioncount}{4}
}
|
