1 \documentclass[12pt,a4paper,fleqn]{report}
2 \usepackage{latexsym,graphicx}
3 \usepackage[refpage]{nomencl}
4 \usepackage{../iman,../extra,../isar,../proof}
5 \usepackage[nohyphen,strings]{../underscore}
6 \usepackage{../isabelle,../isabellesym}
8 \usepackage{../pdfsetup}
11 \hyphenation{Isabelle}
15 \title{\includegraphics[scale=0.5]{isabelle_isar}
16 \\[4ex] The Isabelle/Isar Implementation}
17 \author{\emph{Makarius Wenzel} \\[3ex]
31 We describe the key concepts underlying the Isabelle/Isar
32 implementation, including ML references for the most important
33 functions. The aim is to give some insight into the overall system
34 architecture, and provide clues on implementing applications within
41 {\small\em Isabelle was not designed; it evolved. Not everyone
42 likes this idea. Specification experts rightly abhor
43 trial-and-error programming. They suggest that no one should
44 write a program without first writing a complete formal
45 specification. But university departments are not software houses.
46 Programs like Isabelle are not products: when they have served
47 their purpose, they are discarded.}
49 Lawrence C. Paulson, ``Isabelle: The Next 700 Theorem Provers''
53 {\small\em As I did 20 years ago, I still fervently believe that the
54 only way to make software secure, reliable, and fast is to make it
55 small. Fight features.}
61 {\small\em One thing that UNIX does not need is more features. It is
62 successful in part because it has a small number of good ideas
63 that work well together. Merely adding features does not make it
64 easier for users to do things --- it just makes the manual
65 thicker. The right solution in the right place is always more
66 effective than haphazard hacking.}
68 Rob Pike and Brian W. Kernighan
72 \thispagestyle{empty}\clearpage
79 \input{Thy/document/Prelim.tex}
80 \input{Thy/document/Logic.tex}
81 \input{Thy/document/Tactic.tex}
82 \input{Thy/document/Proof.tex}
83 \input{Thy/document/Syntax.tex}
84 \input{Thy/document/Isar.tex}
85 \input{Thy/document/Local_Theory.tex}
86 \input{Thy/document/Integration.tex}
89 \input{Thy/document/ML.tex}
93 \bibliographystyle{abbrv} \small\raggedright\frenchspacing
94 \bibliography{../manual}