helm/papers/whelp/moogle.aux

   1 \relax
   2 \ifx\hyper@anchor\@undefined
   3 \global \let \oldcontentsline\contentsline
   4 \gdef \contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}
   5 \global \let \oldnewlabel\newlabel
   6 \gdef \newlabel#1#2{\newlabelxx{#1}#2}
   7 \gdef \newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
   8 \AtEndDocument{\let \contentsline\oldcontentsline
   9 \let \newlabel\oldnewlabel}
  10 \else
  11 \global \let \hyper@last\relax
  12 \fi
  13
  14 \citation{pechino}
  15 \citation{coq}
  16 \citation{McCune}
  17 \citation{Graf}
  18 \citation{Ganzinger}
  19 \citation{metadata1}
  20 \citation{metadata2}
  21 \citation{disambiguation}
  22 \citation{metadata1}
  23 \@writefile{toc}{\contentsline {title}{A content based mathematical search engine: Whelp}{1}{chapter.1}}
  24 \@writefile{toc}{\contentsline {author}{Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen,\unskip \ \ignorespaces  Enrico Tassi, and Stefano Zacchiroli}{1}{chapter.1}}
  25 \@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{1}{section.1.1}}
  26 \newlabel{sec:intro}{{1}{1}{Introduction\relax }{section.1.1}{}}
  27 \@writefile{toc}{\contentsline {section}{\numberline {2}Syntax}{2}{section.1.2}}
  28 \newlabel{sec:syntax}{{2}{2}{Syntax\relax }{section.1.2}{}}
  29 \@writefile{lot}{\contentsline {table}{\numberline {1}{\ignorespaces Whelp's term syntax}}{2}{table.1.1}}
  30 \newlabel{tab:syntax}{{1}{2}{Syntax\relax }{table.1.1}{}}
  31 \@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Whelp's processing}}{3}{figure.1.1}}
  32 \newlabel{fig:engine}{{1}{3}{Syntax\relax }{figure.1.1}{}}
  33 \@writefile{toc}{\contentsline {section}{\numberline {3}Disambiguation}{3}{section.1.3}}
  34 \newlabel{sec:disambiguation}{{3}{3}{Disambiguation\relax }{section.1.3}{}}
  35 \citation{munoz}
  36 \citation{mcbride}
  37 \citation{disambiguation}
  38 \@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces  Disambiguation: interpretation choice}}{5}{figure.1.2}}
  39 \newlabel{fig:disambiguation}{{2}{5}{Disambiguation\relax }{figure.1.2}{}}
  40 \@writefile{toc}{\contentsline {section}{\numberline {4}Metadata}{5}{section.1.4}}
  41 \newlabel{sec:metadata}{{4}{5}{Metadata\relax }{section.1.4}{}}
  42 \citation{edinburgh}
  43 \@writefile{toc}{\contentsline {section}{\numberline {5}Whelp{} Queries}{7}{section.1.5}}
  44 \newlabel{sec:queries}{{5}{7}{\whelp {} Queries\relax }{section.1.5}{}}
  45 \@writefile{toc}{\contentsline {subsection}{\numberline {5.1}\textsc  {Match}}{7}{subsection.1.5.1}}
  46 \newlabel{sec:match}{{5.1}{7}{\match \relax }{subsection.1.5.1}{}}
  47 \@writefile{toc}{\contentsline {subsubsection}{Matching Incomplete Patterns}{8}{section*.1}}
  48 \@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces  \textsc  {Match}{} results.}}{9}{figure.1.3}}
  49 \newlabel{fig:match}{{3}{9}{Matching Incomplete Patterns\relax }{figure.1.3}{}}
  50 \@writefile{toc}{\contentsline {subsection}{\numberline {5.2}\textsc  {Hint}}{9}{subsection.1.5.2}}
  51 \newlabel{sec:hint}{{5.2}{9}{\hint \relax }{subsection.1.5.2}{}}
  52 \newlabel{eq:hint1}{{1}{9}{\hint \relax }{equation.1}{}}
  53 \newlabel{eq:hint2}{{2}{9}{\hint \relax }{equation.2}{}}
  54 \citation{metadata2}
  55 \citation{McCune}
  56 \citation{Graf}
  57 \citation{Ganzinger}
  58 \citation{metadata1}
  59 \citation{metadata2}
  60 \citation{mcbride}
  61 \@writefile{toc}{\contentsline {subsection}{\numberline {5.3}\textsc  {Elim}}{10}{subsection.1.5.3}}
  62 \newlabel{sec:elim}{{5.3}{10}{\elim \relax }{subsection.1.5.3}{}}
  63 \@writefile{toc}{\contentsline {subsection}{\numberline {5.4}\textsc  {Locate}}{11}{subsection.1.5.4}}
  64 \newlabel{sec:locate}{{5.4}{11}{\locate \relax }{subsection.1.5.4}{}}
  65 \citation{annals}
  66 \@writefile{toc}{\contentsline {section}{\numberline {6}Web Interface}{12}{section.1.6}}
  67 \newlabel{sec:interface}{{6}{12}{Web Interface\relax }{section.1.6}{}}
  68 \citation{exportation}
  69 \citation{C-Corn}
  70 \@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces  Whelp's HTTP pipeline.}}{13}{figure.1.4}}
  71 \newlabel{fig:http}{{4}{13}{Web Interface\relax }{figure.1.4}{}}
  72 \@writefile{toc}{\contentsline {section}{\numberline {7}Conclusions}{13}{section.1.7}}
  73 \newlabel{sec:conclusions}{{7}{13}{Conclusions\relax }{section.1.7}{}}
  74 \citation{iso1,iso2}
  75 \citation{mizarbrowsing,mizarsearchengine}
  76 \citation{cairns}
  77 \bibcite{edinburgh}{1}
  78 \bibcite{annals}{2}
  79 \bibcite{metadata2}{3}
  80 \bibcite{pechino}{4}
  81 \bibcite{mizarsearchengine}{5}
  82 \bibcite{mizarbrowsing}{6}
  83 \bibcite{cairns}{7}
  84 \bibcite{coq}{8}
  85 \bibcite{C-Corn}{9}
  86 \bibcite{iso1}{10}
  87 \bibcite{iso2}{11}
  88 \bibcite{Ganzinger}{12}
  89 \bibcite{Graf}{13}
  90 \bibcite{metadata1}{14}
  91 \bibcite{mcbride}{15}
  92 \bibcite{McCune}{16}
  93 \bibcite{munoz}{17}
  94 \bibcite{exportation}{18}
  95 \bibcite{disambiguation}{19}