1\documentclass[11pt,a4paper]{article} 2\usepackage{lmodern} 3\usepackage[T1]{fontenc} 4\usepackage{tikz} 5\usepackage{subfigure} 6\usepackage[nohyphen,strings]{underscore} 7\usepackage{amsmath} 8\usepackage{isabelle,isabellesym} 9\usepackage{verbatim} 10\usepackage{alltt} 11\usepackage{array} 12 13\usepackage{amssymb} 14 15\usepackage{pdfsetup} 16 17\isadroptag{theory} 18\isafoldtag{proof} 19 20% urls in roman style, theory text in typewriter 21\urlstyle{rm} 22\isabellestyle{tt} 23 24 25\begin{document} 26 27\title{Tutorial to Locales and Locale Interpretation% 28\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.}} 29\author{Clemens Ballarin} 30\date{} 31 32\maketitle 33 34\begin{abstract} 35 Locales are Isabelle's approach for dealing with parametric 36 theories. They have been designed as a module system for a 37 theorem prover that can adequately represent the complex 38 inter-dependencies between structures found in abstract algebra, but 39 have proven fruitful also in other applications --- for example, 40 software verification. 41 42 Both design and implementation of locales have evolved considerably 43 since Kamm\"uller did his initial experiments. Today, locales 44 are a simple yet powerful extension of the Isar proof language. 45 The present tutorial covers all major facilities of locales. It is 46 intended for locale novices; familiarity with Isabelle and Isar is 47 presumed. 48\end{abstract} 49 50\parindent 0pt\parskip 0.5ex 51 52\input{session} 53 54\bibliographystyle{abbrv} 55\bibliography{root} 56 57\end{document} 58 59%%% Local Variables: 60%%% mode: latex 61%%% TeX-master: t 62%%% End: 63