@InProceedings{	  luth.ea:tas:2000,
  author	= {Christoph L{\"u}th and Burkhart Wolff},
  title		= {{TAS} --- A Generic Window Inference System},
  editor	= {J. Harrison and M. Aagaard},
  booktitle	= {Theorem Proving in Higher Order Logics: 13th International
		  classification = {proceedings}, Conference, TPHOLs 2000},
  year		= 2000,
  series	= {Lecture Notes in Computer Science},
  pages		= {405--422},
  publisher	= {Springer Verlag},
  number	= 1869,
  ps		= {papers/2000/TAS.ps.gz},
  pdf		= {papers/2000/TAS.pdf.gz},
  language	= {USenglish},
  abstract	= {This paper presents work on technology for
		  transformational proof and program development, as used by
		  window inference calculi and transformation systems. The
		  calculi are characterised by a certain class of theorems in
		  the underlying logic. Our transformation system TAS
		  compiles these rules to concrete deduction support,
		  complete with a graphical user interface with
		  command-language-free user interaction by gestures like
		  drag&drop and proof-by-pointing, and a development
		  management for transformational proofs. It is
		  <em>generic</eM> in the sense that it is completely
		  independent of the particular window inference or
		  transformational calculus, and can be instantiated to many
		  different ones; three such instantiations are presented in
		  the paper.}
}

@InProceedings{	  luth.ea:tas:2000,
  author	= {Christoph L{\"u}th and Burkhart Wolff},
  title		= {{TAS} --- A Generic Window Inference System},
  editor	= {J. Harrison and M. Aagaard},
  booktitle	= {Theorem Proving in Higher Order Logics: 13th International
		  Conference, TPHOLs 2000},
  year		= 2000,
  classification= {proceedings},
  series	= {Lecture Notes in Computer Science},
  pages		= {405--422},
  publisher	= {Springer Verlag},
  number	= 1869,
  ps		= {papers/2000/TAS.ps.gz},
  pdf		= {papers/2000/TAS.pdf.gz},
  language	= {USenglish},
  abstract	= {This paper presents work on technology for
		  transformational proof and program development, as used by
		  window inference calculi and transformation systems. The
		  calculi are characterised by a certain class of theorems in
		  the underlying logic. Our transformation system TAS
		  compiles these rules to concrete deduction support,
		  complete with a graphical user interface with
		  command-language-free user interaction by gestures like
		  drag&amp;drop and proof-by-pointing, and a development
		  management for transformational proofs. It is
		  <em>generic</eM> in the sense that it is completely
		  independent of the particular window inference or
		  transformational calculus, and can be instantiated to many
		  different ones; three such instantiations are presented in
		  the paper.}
}