X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fwhelp%2Fmoogle.aux;fp=helm%2Fpapers%2Fwhelp%2Fmoogle.aux;h=0000000000000000000000000000000000000000;hb=85747dc6d0578b484544bb8120aad7aa89813f27;hp=8c75054b2523675aab7b23bee74d88537205a8fc;hpb=c1986639552e01334a05db4236627a6c1ffacf21;p=helm.git

diff --git a/helm/papers/whelp/moogle.aux b/helm/papers/whelp/moogle.aux
deleted file mode 100644
index 8c75054b2..000000000
--- a/helm/papers/whelp/moogle.aux
+++ /dev/null
@@ -1,95 +0,0 @@
-\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}