@InCollection{	  wenzel.ea:building:2007,
  abstract	= {We present the generic system framework of
		  Isabelle/Isarunderlying recent versions of Isabelle. Among
		  other things, Isar provides an infrastructure for Isabelle
		  plug-ins, comprising extensible state components and
		  extensible syntax that can be bound to tactical ML
		  programs. Thus the Isabelle/Isar architecture may be
		  understood as an extension and refinement of the
		  traditional “LCF approach”, with explicit infrastructure
		  for building derivative systems. To demonstrate the
		  technical potential of the framework, we apply it to a
		  concrete formalmethods tool: the HOL-Z 3.0 environment,
		  which is geared towards the analysis of Z specifications
		  and formal proof of forward-refinements.},
  author	= {Makarius Wenzel and Burkhart Wolff},
  booktitle	= {TPHOLs 2007},
  copyright	= {\copyright Springer-Verlag},
  editor	= {Klaus Schneider and Jens Brandt},
  language	= {USenglish},
  pages		= {351--366},
  pdf		= {papers/2007/tphols07.submission.pdf},
  publisher	= {Springer-Verlag},
  series	= {LNCS 4732},
  title		= {Building Formal Method Tools in the Isabelle/Isar
		  Framework},
  year		= 2007,
  user		= {wolff}
}