| author | wenzelm | 
| Thu, 14 Apr 2016 12:00:29 +0200 | |
| changeset 62972 | 0eedd78c2b47 | 
| parent 61409 | 9d68db31196c | 
| child 70112 | 7721589f3efd | 
| permissions | -rw-r--r-- | 
| 53769 | 1  | 
\documentclass[12pt,a4paper]{report}
 | 
| 
60185
 
cc71f01f9fde
prefer lmodern, which produces scalable T1 fonts even with Debian-ized TeXLive;
 
wenzelm 
parents: 
57327 
diff
changeset
 | 
2  | 
\usepackage{lmodern}
 | 
| 
57002
 
97a80d41a5ba
prefer T1 with searchable underscore (requires proper cm-super fonts);
 
wenzelm 
parents: 
54356 
diff
changeset
 | 
3  | 
\usepackage[T1]{fontenc}
 | 
| 53769 | 4  | 
\usepackage{supertabular}
 | 
5  | 
\usepackage{graphicx}
 | 
|
| 61409 | 6  | 
\usepackage{iman,extra,isar}
 | 
| 53769 | 7  | 
\usepackage[nohyphen,strings]{underscore}
 | 
| 57327 | 8  | 
\usepackage{amssymb}
 | 
| 53769 | 9  | 
\usepackage{isabelle,isabellesym}
 | 
10  | 
\usepackage{railsetup}
 | 
|
11  | 
\usepackage{style}
 | 
|
12  | 
\usepackage{pdfsetup}
 | 
|
13  | 
||
| 57310 | 14  | 
\hyphenation{Edinburgh}
 | 
| 53769 | 15  | 
\hyphenation{Isabelle}
 | 
16  | 
\hyphenation{Isar}
 | 
|
17  | 
||
18  | 
\isadroptag{theory}
 | 
|
19  | 
||
20  | 
\isabellestyle{literal}
 | 
|
| 
61408
 
9020a3ba6c9a
@{verbatim [display]} supersedes old alltt/ttbox;
 
wenzelm 
parents: 
60185 
diff
changeset
 | 
21  | 
\def\isastylett{\footnotesize\tt}
 | 
| 53769 | 22  | 
|
| 53775 | 23  | 
\title{\includegraphics[scale=0.5]{isabelle_jedit} \\[4ex] Isabelle/jEdit}
 | 
| 53769 | 24  | 
|
25  | 
\author{\emph{Makarius Wenzel}}
 | 
|
26  | 
||
27  | 
\makeindex  | 
|
28  | 
||
29  | 
||
30  | 
\begin{document}
 | 
|
31  | 
||
32  | 
\maketitle  | 
|
| 
53770
 
db362319d766
added/updated material from src/Tools/jEdit/README.html;
 
wenzelm 
parents: 
53769 
diff
changeset
 | 
33  | 
|
| 53776 | 34  | 
\begin{abstract}
 | 
35  | 
Isabelle/jEdit is a fully-featured Prover IDE, based on Isabelle/Scala and  | 
|
36  | 
the jEdit text editor. This document provides an overview of general  | 
|
37  | 
principles and its main IDE functionality.  | 
|
38  | 
\end{abstract}
 | 
|
39  | 
||
40  | 
\vspace*{2.5cm}
 | 
|
41  | 
||
42  | 
\begin{quote}
 | 
|
43  | 
  {\small\em Isabelle's user interface is no advance over LCF's, which is
 | 
|
44  | 
widely condemned as ``user-unfriendly'': hard to use, bewildering to  | 
|
45  | 
beginners. Hence the interest in proof editors, where a proof can be  | 
|
46  | 
constructed and modified rule-by-rule using windows, mouse, and menus. But  | 
|
47  | 
Edinburgh LCF was invented because real proofs require millions of  | 
|
48  | 
inferences. Sophisticated tools --- rules, tactics and tacticals, the  | 
|
49  | 
language ML, the logics themselves --- are hard to learn, yet they are  | 
|
50  | 
essential. We may demand a mouse, but we need better education and  | 
|
51  | 
training.}  | 
|
52  | 
||
53  | 
Lawrence C. Paulson, ``Isabelle: The Next 700 Theorem Provers''  | 
|
54  | 
\end{quote}
 | 
|
55  | 
||
56  | 
||
57  | 
\vspace*{2.5cm}
 | 
|
58  | 
||
| 
53770
 
db362319d766
added/updated material from src/Tools/jEdit/README.html;
 
wenzelm 
parents: 
53769 
diff
changeset
 | 
59  | 
|
| 
 
db362319d766
added/updated material from src/Tools/jEdit/README.html;
 
wenzelm 
parents: 
53769 
diff
changeset
 | 
60  | 
\subsubsection*{Acknowledgements}
 | 
| 
 
db362319d766
added/updated material from src/Tools/jEdit/README.html;
 
wenzelm 
parents: 
53769 
diff
changeset
 | 
61  | 
|
| 
 
db362319d766
added/updated material from src/Tools/jEdit/README.html;
 
wenzelm 
parents: 
53769 
diff
changeset
 | 
62  | 
Research and implementation of concepts around PIDE and Isabelle/jEdit has  | 
| 57310 | 63  | 
started in 2008 and was kindly supported by:  | 
| 
53770
 
db362319d766
added/updated material from src/Tools/jEdit/README.html;
 
wenzelm 
parents: 
53769 
diff
changeset
 | 
64  | 
\begin{itemize}
 | 
| 54320 | 65  | 
\item TU M\"unchen \url{http://www.in.tum.de}
 | 
| 
53770
 
db362319d766
added/updated material from src/Tools/jEdit/README.html;
 
wenzelm 
parents: 
53769 
diff
changeset
 | 
66  | 
\item BMBF \url{http://www.bmbf.de}
 | 
| 
 
db362319d766
added/updated material from src/Tools/jEdit/README.html;
 
wenzelm 
parents: 
53769 
diff
changeset
 | 
67  | 
\item Universit\'e Paris-Sud \url{http://www.u-psud.fr}
 | 
| 
 
db362319d766
added/updated material from src/Tools/jEdit/README.html;
 
wenzelm 
parents: 
53769 
diff
changeset
 | 
68  | 
\item Digiteo \url{http://www.digiteo.fr}
 | 
| 
 
db362319d766
added/updated material from src/Tools/jEdit/README.html;
 
wenzelm 
parents: 
53769 
diff
changeset
 | 
69  | 
\item ANR \url{http://www.agence-nationale-recherche.fr}
 | 
| 
 
db362319d766
added/updated material from src/Tools/jEdit/README.html;
 
wenzelm 
parents: 
53769 
diff
changeset
 | 
70  | 
\end{itemize}
 | 
| 
 
db362319d766
added/updated material from src/Tools/jEdit/README.html;
 
wenzelm 
parents: 
53769 
diff
changeset
 | 
71  | 
|
| 
 
db362319d766
added/updated material from src/Tools/jEdit/README.html;
 
wenzelm 
parents: 
53769 
diff
changeset
 | 
72  | 
|
| 54356 | 73  | 
\pagenumbering{roman}
 | 
74  | 
\tableofcontents  | 
|
75  | 
\listoffigures  | 
|
76  | 
\clearfirst  | 
|
| 53769 | 77  | 
|
78  | 
\input{JEdit.tex}
 | 
|
79  | 
||
80  | 
\begingroup  | 
|
81  | 
  \tocentry{\bibname}
 | 
|
82  | 
  \bibliographystyle{abbrv} \small\raggedright\frenchspacing
 | 
|
83  | 
  \bibliography{manual}
 | 
|
84  | 
\endgroup  | 
|
85  | 
||
86  | 
\tocentry{\indexname}
 | 
|
87  | 
\printindex  | 
|
88  | 
||
89  | 
\end{document}
 |