4 \documentclass[12pt,a4paper,fleqn]{report}
5 \usepackage{latexsym,graphicx}
6 \usepackage[refpage]{nomencl}
7 \usepackage{../iman,../extra,../isar,../proof}
8 \usepackage{Thy/document/isabelle,Thy/document/isabellesym}
10 \usepackage{../pdfsetup}
13 \hyphenation{Isabelle}
17 \title{\includegraphics[scale=0.5]{isabelle_isar}
18 \\[4ex] The Isabelle/Isar Implementation}
19 \author{\emph{Makarius M. M. Wenzel}}
30 We describe the key concepts underlying the Isabelle/Isar
31 implementation, including ML references for the most important
32 elements. The aim is to give some insight into the overall system
33 architecture, and provide clues on implementing user extensions.
36 \pagenumbering{roman} \tableofcontents \clearfirst
39 \input{Thy/document/prelim.tex}
40 \input{Thy/document/logic.tex}
41 \input{Thy/document/tactic.tex}
42 \input{Thy/document/proof.tex}
43 \input{Thy/document/locale.tex}
44 \input{Thy/document/integration.tex}
46 % Isabelle was not designed; it evolved.
47 % Not everyone likes this idea. Specification experts rightly abhor trial-and-error programming.
48 % They suggest that no one should write a program without First writing a complete
49 % formal specification. But university departments are not software houses. Programs like
50 % Isabelle are not products: when they have served their purpose, they are discarded.
52 % L.C. Paulson, Isabelle: The Next 700 Theorem Provers
55 \input{Thy/document/ML.tex}
59 \bibliographystyle{plain} \small\raggedright\frenchspacing
60 \bibliography{../manual}
63 \tocentry{\glossaryname}