\begin{thebibliography}{10}

\bibitem{TPS}
P.B. Andrews, M.~Bishop, and C.E. Brown.
\newblock System description: {TPS}: A theorem proving system for type theory.
\newblock In {\em Proc.\ of the 17th {Int.\ Conf.\ on {A}utomated {D}eduction
  (CADE-17)}}, LNCS, pages 164--169. Springer, 2000.

\bibitem{VSE98}
S.~Autexier, D.~Hutter, B.~Langenstein, H.~Mantel, G.~Rock, A.~Schairer,
  W.~Stephan, R.~Vogt, and A.~Wolpers.
\newblock {VSE}: Formal methods meet industrial needs.
\newblock {\em International Journal on Software Tools for Technology Transfer,
  Special issue on Mechanized Theorem Proving for Technology, Springer},
  september 1998.

\bibitem{quodlibet}
J.~Avenhaus, U.~K{\"u}hler, T.~Schmidt-Samoa, and C.-P. Wirth.
\newblock How to prove inductive theorems? {\QUODLIBET}!
\newblock In {\em Proc.\ of the 19th {Int.\ Conf.\ on {A}utomated {D}eduction
  (CADE-19)}}, number 2741 in LNAI, pages 328--333. Springer, 2003.

\bibitem{COQ}
Y.~Bertot and P.~Cast{\'e}ran.
\newblock {\em Interactive Theorem Proving and Program Development --- Coq'Art:
  The Calculus of Inductive Constructions}.
\newblock Texts in Theoretical Computer Science, An EATCS Series. Springer,
  2004.

\bibitem{ChSo00}
L.~Cheikhrouhou and V.~Sorge.
\newblock {PDS --- A Three-Dimensional Data Structure for Proof Plans}.
\newblock In {\em Proc.\ of the {Int.\ Conf.\ on Artificial and Computational
  Intelligence for Decision, Control and Automation} in Engineering and
  Industrial Applications (ACIDCA'2000)}, 2000.

\bibitem{Di-05-a}
L.~Dixon.
\newblock Interactive and hierarchical tracing of techniques in {IsaPlanner}.
\newblock In {\em Proc.\ of UITP'05}, 2005.

\bibitem{Fiedler:ijcai01}
A.~Fiedler.
\newblock Dialog-driven adaptation of explanations of proofs.
\newblock In {\em Proc.\ of the 17th {I}nternational {J}oint {C}onference on
  {A}rtificial {I}ntelligence ({IJCAI})}, pages 1295--1300, Seattle, WA, 2001.
  Morgan Kaufmann.

\bibitem{omega02}
The~OMEGA Group.
\newblock Proof development with {\OMEGA}.
\newblock In {\em Proc.\ of the 18th {Int.\ Conf.\ on {A}utomated {D}eduction
  (CADE-18)}}, number 2392 in LNAI, pages 143--148. Springer, 2002.

\bibitem{Huang94a}
X.~Huang.
\newblock Reconstructing proofs at the assertion level.
\newblock In {\em Proc.\ of the 12th {Int.\ Conf.\ on {A}utomated {D}eduction
  (CADE-12)}}, LNAI, pages 738--752. Springer, 1994.

\bibitem{J09}
M.~H\"ubner, S.~Autexier, C.~Benzm{\"u}ller, and A.~Meier.
\newblock Interactive theorem proving with tasks.
\newblock {\em Electronic Notes in Theoretical Computer Science},
  103(C):161--181, November 2004.

\bibitem{HuSe-96-a}
D.~Hutter and C.~Sengler.
\newblock {INKA - The Next Generation}.
\newblock In {\em Proc.\ of the 13th {I}nternational {C}onference on
  {A}utomated {D}eduction (CADE--13)}, LNAI. Springer, 1996.

\bibitem{nuprl}
C.~Kreitz, L.~Lorigo, R.~Eaton, R.L. Constable, and S.F. Allen.
\newblock The nuprl open logical environment, 2000.

\bibitem{multi}
Andreas Meier.
\newblock {\em Proof Planning with Multiple Strategies}.
\newblock PhD thesis, Saarland Univ., 2004.

\bibitem{MelisSiekmann99}
E.~Melis and J.~Siekmann.
\newblock {Knowledge-Based Proof Planning}.
\newblock {\em Artificial Intelligence}, 115(1):65--105, 1999.

\bibitem{Paulson94}
L.C. Paulson.
\newblock {\em Isabelle: {A} Generic Theorem Prover}.
\newblock LNCS. Springer, 1994.

\bibitem{B1}
J.~Siekmann, C.~Benzm{\"u}ller, A.~Fiedler, A~Meier, I.~Normann, and M.~Pollet.
\newblock {\em Proof Development in {OMEGA}: The Irrationality of Square Root
  of 2}, pages 271--314.
\newblock Kluwer Academic Publishers, 2003.

\bibitem{lpar02}
J.~Siekmann, C.~Benzm{\"u}ller, A.~Fiedler, A.~Meier, and M.~Pollet.
\newblock Proof development with {OMEGA}: Sqrt(2) is irrational.
\newblock In {\em Logic for Programming, Artificial Intelligence, and
  Reasoning, 9th {Int.\ Conf., LPAR 2002}}, number 2514 in LNAI, pages
  367--387. Springer, 2002.

\bibitem{ags-2003-d-15}
C.-P. Wirth.
\newblock Descente infinie + {D}eduction.
\newblock {\em Logic J. of the IGPL}, 12(1):1--96, 2004.

\end{thebibliography}