author wenzelm
Sat, 05 Apr 2014 15:03:40 +0200
changeset 56421 1ffd7eaa778b
parent 48985 5386df44a037
child 57002 97a80d41a5ba
permissions -rw-r--r--
updated to jedit_build-20140405: Code2HTML.jar, CommonControls.jar, Console.jar, kappalayout.jar, Navigator.jar, SideKick.jar, doc with jEdit manuals (ant dist-manuals);






% urls in roman style, theory text in typewriter


\title{Tutorial to Locales and Locale Interpretation%
\thanks{Published in L.~Lamb\'an, A.~Romero, J.~Rubio, editors, {\em Contribuciones Cient\'{\i}ficas en honor de Mirian Andr\'es.}  Servicio de Publicaciones de la Universidad de La Rioja, Logro\~no, Spain, 2010.  Reproduced by permission.}}
\author{Clemens Ballarin}


  Locales are Isabelle's approach for dealing with parametric
  theories.  They have been designed as a module system for a
  theorem prover that can adequately represent the complex
  inter-dependencies between structures found in abstract algebra, but
  have proven fruitful also in other applications --- for example,
  software verification.

  Both design and implementation of locales have evolved considerably
  since Kamm\"uller did his initial experiments.  Today, locales
  are a simple yet powerful extension of the Isar proof language.
  The present tutorial covers all major facilities of locales.  It is
  intended for locale novices; familiarity with Isabelle and Isar is

\parindent 0pt\parskip 0.5ex




%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: