(TeX-add-style-hook "eprover"
 (lambda ()
    (LaTeX-add-index-entries
     "xyzzy"
     "terms"
     "variables"
     "subterm"
     "equations"
     "literal"
     "ordering"
     "reduction ordering"
     "selection functions"
     "literals!eligible"
     "eligible for paramodulation|see{literals, eligible}"
     "eligible for resolution|see{literals, eligible}"
     "eligible literals|see{literals, eligible}"
     "SP@\\textbf{SP} (calculus)"
     "equality resolution"
     "superposition"
     "equality factoring"
     "rewriting"
     "E (theorem prover)"
     "SPASS"
     "subsumption"
     "simplify-reflect"
     "contextual
       simplify-reflect"
     "tautology deletion"
     "equality
     resolution"
     "clause splitting"
     "DISCOUNT"
     "proof procedure"
     "clause evaluation"
     "term ordering"
     "GPL"
     "GNU General Public
    License"
     "LGPL"
     "GNU Lesser General Public License")
    (LaTeX-add-bibitems
     "Bachmair:personal-98"
     "BDP89"
     "BG94"
     "CL73"
     "Dershowitz:IJCAI-91"
     "DKS97"
     "DS94a"
     "DS94b"
     "DS96a"
     "BHF96"
     "HJL:CADE-99"
     "Mc94"
     "MILSGSM:JAR-97"
     "MW:JAR-97"
     "NN:RTA-93"
     "RV:IJCAR-2001"
     "RV:AICOM-2002"
     "E:WWW-99"
     "Schulz:Diss-2000"
     "Schulz:KI-2001"
     "Schulz:AICOM-2002"
     "Schulz:IJCAR-2004"
     "GSCG:IJCAR-2006"
     "Sutcliffe:TPTP-WWW"
     "Tammet:JAR-97"
     "WABCEKTT:CADE-99"
     "Weidenbach:personal-99"
     "Weidenbach:SPASS-2001"
     "WGR96")
    (LaTeX-add-labels
     "sec:intro"
     "sec:start"
     "sec:calculus"
     "def:basics:inferences:selection"
     "def:basics:inferences:eligible"
     "def:basics:inferences:sp"
     "sec:procedure"
     "fig:procedure"
     "sec:options"
     "sec:options:heuristics"
     "sec:options:orderings"
     "sec:options:strategies"
     "sec:options:watchlist"
     "sec:options:learning"
     "sec:options:others"
     "sec:language"
     "sec:output"
     "sec:output:essentials"
     "sec:output:normal"
     "sec:output:lots"
     "sec:output:results")
    (TeX-add-symbols
     '("etalchar" 1))
    (TeX-run-style-hooks
     "url"
     "supertabular"
     "estyle"
     "makeidx"
     "latex2e"
     "art10"
     "article")))