@InCollection{AhrendtBeckertEAChap98,	  
  author	= {Wolfgang Ahrendt and Bernhard Beckert and Reiner
		  H\"ahnle and Wolfram Menzel and Wolfgang Reif and
		  Gerhard Schellhorn and Peter H. Schmitt},
  title		= {Integrating Automated and Interactive Theorem Proving},
  part  	= {1: Interactive Theorem Proving},
  volume        = {{II}: Systems and Implementation Techniques},
  chapter       = {4},
  pages         = {97--116},		  
  booktitle	= {Automated Deduction --- A Basis for Applications},
  editor	= {Wolfgang Bibel and Peter H. Schmitt},
  publisher	= {Kluwer, Dordrecht},
  year		= {1998}
}