1\documentclass[12pt,a4paper,fleqn]{report} 2\usepackage{lmodern} 3\usepackage[T1]{fontenc} 4\usepackage{latexsym,graphicx} 5\usepackage[refpage]{nomencl} 6\usepackage{iman,extra,isar,proof} 7\usepackage[nohyphen,strings]{underscore} 8\usepackage{isabelle} 9\usepackage{isabellesym} 10\usepackage{railsetup} 11\usepackage{supertabular} 12\usepackage{style} 13\usepackage{pdfsetup} 14 15 16\hyphenation{Isabelle} 17\hyphenation{Isar} 18 19\isadroptag{theory} 20\title{\includegraphics[scale=0.5]{isabelle_isar} 21 \\[4ex] The Isabelle/Isar Implementation} 22\author{\emph{Makarius Wenzel} \\[3ex] 23 With Contributions by 24 Stefan Berghofer, \\ 25 Florian Haftmann 26 and Larry Paulson 27} 28 29\makeindex 30 31 32\begin{document} 33 34\maketitle 35 36\begin{abstract} 37 We describe the key concepts underlying the Isabelle/Isar 38 implementation, including ML references for the most important 39 functions. The aim is to give some insight into the overall system 40 architecture, and provide clues on implementing applications within 41 this framework. 42\end{abstract} 43 44\vspace*{2.5cm} 45\begin{quote} 46 47 {\small\em Isabelle was not designed; it evolved. Not everyone 48 likes this idea. Specification experts rightly abhor 49 trial-and-error programming. They suggest that no one should 50 write a program without first writing a complete formal 51 specification. But university departments are not software houses. 52 Programs like Isabelle are not products: when they have served 53 their purpose, they are discarded.} 54 55 Lawrence C. Paulson, ``Isabelle: The Next 700 Theorem Provers'' 56 57 \vspace*{1cm} 58 59 {\small\em As I did 20 years ago, I still fervently believe that the 60 only way to make software secure, reliable, and fast is to make it 61 small. Fight features.} 62 63 Andrew S. Tanenbaum 64 65 \vspace*{1cm} 66 67 {\small\em One thing that UNIX does not need is more features. It is 68 successful in part because it has a small number of good ideas 69 that work well together. Merely adding features does not make it 70 easier for users to do things --- it just makes the manual 71 thicker. The right solution in the right place is always more 72 effective than haphazard hacking.} 73 74 Rob Pike and Brian W. Kernighan 75 76 \vspace*{1cm} 77 78 {\small\em If you look at software today, through the lens of the 79 history of engineering, it's certainly engineering of a sort--but 80 it's the kind of engineering that people without the concept of 81 the arch did. Most software today is very much like an Egyptian 82 pyramid with millions of bricks piled on top of each other, with 83 no structural integrity, but just done by brute force and 84 thousands of slaves.} 85 86 Alan Kay 87 88\end{quote} 89 90\thispagestyle{empty}\clearpage 91 92\pagenumbering{roman} 93\tableofcontents 94\listoffigures 95\clearfirst 96 97\setcounter{chapter}{-1} 98 99\input{ML.tex} 100\input{Prelim.tex} 101\input{Logic.tex} 102\input{Syntax.tex} 103\input{Tactic.tex} 104\input{Eq.tex} 105\input{Proof.tex} 106\input{Isar.tex} 107\input{Local_Theory.tex} 108\input{Integration.tex} 109 110\begingroup 111\tocentry{\bibname} 112\bibliographystyle{abbrv} \small\raggedright\frenchspacing 113\bibliography{manual} 114\endgroup 115 116\tocentry{\indexname} 117\printindex 118 119\end{document} 120 121 122%%% Local Variables: 123%%% mode: latex 124%%% TeX-master: t 125%%% End: 126