@InProceedings{	  luth.ea:more:2000,
  author	= {Christoph L{\"u}th and Burkhart Wolff},
  title		= {More about {TAS} and {IsaWin}: Tools for Formal Program
		  Development},
  editor	= {T. Maibaum},
  booktitle	= {Fundamental Approaches to Software Engineering {FASE 200}.
		  Joint European Conferences on Theory and Practice of
		  Software {ETAPS 2000}},
  year		= 2000,
  language	= {USenglish},
  classification= {proceedings},
  series	= {Lecture Notes in Computer Science},
  pages		= {367-- 370},
  publisher	= {Springer Verlag},
  number	= 1783,
  ps		= {papers/2000/sysdesc.ps.gz},
  pdf		= {papers/2000/sysdesc.pdf.gz},
  abstract	= {We present a family of tools for program development and
		  verification, compris\- ing the transformation system TAS
		  and the theorem proving interface IsaWin. Both are based on
		  the theorem prover Isabelle, which is used as a generic
		  logical framework here. A graphical user interface, based
		  on the principle of di\- rect manipulation, allows the user
		  to interact with the tool without having to concern himself
		  with the details of the representation within the theorem
		  prover, leaving him to concentrate on the main design
		  decisions of program development or theorem proving. The
		  tools form an integrated system for formal program
		  development, in which TAS is used for transformational
		  program development, and IsaWin for discharging the
		  incurred proof obligations. However, both tools can be used
		  sep\- arately as well. Further, the tools are generic over
		  the formal method employed. In this extended abstract, we
		  will first give a brief overview over TAS and IsaWin. Since
		  TAS and IsaWin have been presented on previous ETAPS
		  conferences, the presentation will highlight the new
		  features as sketched out below. }
}