\relax 
\ifx\hyper@anchor\@undefined
\global \let \oldcontentsline\contentsline
\gdef \contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}
\global \let \oldnewlabel\newlabel
\gdef \newlabel#1#2{\newlabelxx{#1}#2}
\gdef \newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
\AtEndDocument{\let \contentsline\oldcontentsline
\let \newlabel\oldnewlabel}
\else
\global \let \hyper@last\relax 
\fi

\citation{pechino}
\citation{coq}
\citation{McCune}
\citation{Graf}
\citation{Ganzinger}
\citation{metadata1}
\citation{metadata2}
\citation{disambiguation}
\citation{metadata1}
\@writefile{toc}{\contentsline {title}{A content based mathematical search engine: Whelp}{1}{chapter.1}}
\@writefile{toc}{\contentsline {author}{Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen,\unskip \ \ignorespaces  Enrico Tassi, and Stefano Zacchiroli}{1}{chapter.1}}
\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{1}{section.1.1}}
\newlabel{sec:intro}{{1}{1}{Introduction\relax }{section.1.1}{}}
\@writefile{toc}{\contentsline {section}{\numberline {2}Syntax}{2}{section.1.2}}
\newlabel{sec:syntax}{{2}{2}{Syntax\relax }{section.1.2}{}}
\@writefile{lot}{\contentsline {table}{\numberline {1}{\ignorespaces Whelp's term syntax}}{2}{table.1.1}}
\newlabel{tab:syntax}{{1}{2}{Syntax\relax }{table.1.1}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Whelp's processing}}{3}{figure.1.1}}
\newlabel{fig:engine}{{1}{3}{Syntax\relax }{figure.1.1}{}}
\@writefile{toc}{\contentsline {section}{\numberline {3}Disambiguation}{3}{section.1.3}}
\newlabel{sec:disambiguation}{{3}{3}{Disambiguation\relax }{section.1.3}{}}
\citation{munoz}
\citation{mcbride}
\citation{disambiguation}
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces  Disambiguation: interpretation choice}}{5}{figure.1.2}}
\newlabel{fig:disambiguation}{{2}{5}{Disambiguation\relax }{figure.1.2}{}}
\@writefile{toc}{\contentsline {section}{\numberline {4}Metadata}{5}{section.1.4}}
\newlabel{sec:metadata}{{4}{5}{Metadata\relax }{section.1.4}{}}
\citation{edinburgh}
\@writefile{toc}{\contentsline {section}{\numberline {5}Whelp{} Queries}{7}{section.1.5}}
\newlabel{sec:queries}{{5}{7}{\whelp {} Queries\relax }{section.1.5}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}\textsc  {Match}}{7}{subsection.1.5.1}}
\newlabel{sec:match}{{5.1}{7}{\match \relax }{subsection.1.5.1}{}}
\@writefile{toc}{\contentsline {subsubsection}{Matching Incomplete Patterns}{8}{section*.1}}
\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces  \textsc  {Match}{} results.}}{9}{figure.1.3}}
\newlabel{fig:match}{{3}{9}{Matching Incomplete Patterns\relax }{figure.1.3}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}\textsc  {Hint}}{9}{subsection.1.5.2}}
\newlabel{sec:hint}{{5.2}{9}{\hint \relax }{subsection.1.5.2}{}}
\newlabel{eq:hint1}{{1}{9}{\hint \relax }{equation.1}{}}
\newlabel{eq:hint2}{{2}{9}{\hint \relax }{equation.2}{}}
\citation{metadata2}
\citation{McCune}
\citation{Graf}
\citation{Ganzinger}
\citation{metadata1}
\citation{metadata2}
\citation{mcbride}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}\textsc  {Elim}}{10}{subsection.1.5.3}}
\newlabel{sec:elim}{{5.3}{10}{\elim \relax }{subsection.1.5.3}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.4}\textsc  {Locate}}{11}{subsection.1.5.4}}
\newlabel{sec:locate}{{5.4}{11}{\locate \relax }{subsection.1.5.4}{}}
\citation{annals}
\@writefile{toc}{\contentsline {section}{\numberline {6}Web Interface}{12}{section.1.6}}
\newlabel{sec:interface}{{6}{12}{Web Interface\relax }{section.1.6}{}}
\citation{exportation}
\citation{C-Corn}
\@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces  Whelp's HTTP pipeline.}}{13}{figure.1.4}}
\newlabel{fig:http}{{4}{13}{Web Interface\relax }{figure.1.4}{}}
\@writefile{toc}{\contentsline {section}{\numberline {7}Conclusions}{13}{section.1.7}}
\newlabel{sec:conclusions}{{7}{13}{Conclusions\relax }{section.1.7}{}}
\citation{iso1,iso2}
\citation{mizarbrowsing,mizarsearchengine}
\citation{cairns}
\bibcite{edinburgh}{1}
\bibcite{annals}{2}
\bibcite{metadata2}{3}
\bibcite{pechino}{4}
\bibcite{mizarsearchengine}{5}
\bibcite{mizarbrowsing}{6}
\bibcite{cairns}{7}
\bibcite{coq}{8}
\bibcite{C-Corn}{9}
\bibcite{iso1}{10}
\bibcite{iso2}{11}
\bibcite{Ganzinger}{12}
\bibcite{Graf}{13}
\bibcite{metadata1}{14}
\bibcite{mcbride}{15}
\bibcite{McCune}{16}
\bibcite{munoz}{17}
\bibcite{exportation}{18}
\bibcite{disambiguation}{19}