| author | wenzelm | 
| Sat, 29 Apr 2017 11:06:39 +0200 | |
| changeset 65633 | 826311fca263 | 
| 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: 
57327diff
changeset | 2 | \usepackage{lmodern}
 | 
| 57002 
97a80d41a5ba
prefer T1 with searchable underscore (requires proper cm-super fonts);
 wenzelm parents: 
54356diff
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: 
60185diff
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: 
53769diff
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: 
53769diff
changeset | 59 | |
| 
db362319d766
added/updated material from src/Tools/jEdit/README.html;
 wenzelm parents: 
53769diff
changeset | 60 | \subsubsection*{Acknowledgements}
 | 
| 
db362319d766
added/updated material from src/Tools/jEdit/README.html;
 wenzelm parents: 
53769diff
changeset | 61 | |
| 
db362319d766
added/updated material from src/Tools/jEdit/README.html;
 wenzelm parents: 
53769diff
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: 
53769diff
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: 
53769diff
changeset | 66 | \item BMBF \url{http://www.bmbf.de}
 | 
| 
db362319d766
added/updated material from src/Tools/jEdit/README.html;
 wenzelm parents: 
53769diff
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: 
53769diff
changeset | 68 | \item Digiteo \url{http://www.digiteo.fr}
 | 
| 
db362319d766
added/updated material from src/Tools/jEdit/README.html;
 wenzelm parents: 
53769diff
changeset | 69 | \item ANR \url{http://www.agence-nationale-recherche.fr}
 | 
| 
db362319d766
added/updated material from src/Tools/jEdit/README.html;
 wenzelm parents: 
53769diff
changeset | 70 | \end{itemize}
 | 
| 
db362319d766
added/updated material from src/Tools/jEdit/README.html;
 wenzelm parents: 
53769diff
changeset | 71 | |
| 
db362319d766
added/updated material from src/Tools/jEdit/README.html;
 wenzelm parents: 
53769diff
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}
 |