1\documentclass[12pt,a4paper]{report} 2\usepackage{lmodern} 3\usepackage[T1]{fontenc} 4\usepackage{supertabular} 5\usepackage{graphicx} 6\usepackage{iman,extra,isar} 7\usepackage[nohyphen,strings]{underscore} 8\usepackage{amssymb} 9\usepackage{isabelle,isabellesym} 10\usepackage{railsetup} 11\usepackage{style} 12\usepackage{pdfsetup} 13 14\hyphenation{Edinburgh} 15\hyphenation{Isabelle} 16\hyphenation{Isar} 17 18\isadroptag{theory} 19 20\isabellestyle{literal} 21\def\isastylett{\footnotesize\tt} 22 23\title{\includegraphics[scale=0.5]{isabelle_jedit} \\[4ex] Isabelle/jEdit} 24 25\author{\emph{Makarius Wenzel}} 26 27\makeindex 28 29 30\begin{document} 31 32\maketitle 33 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 59 60\subsubsection*{Acknowledgements} 61 62Research and implementation of concepts around PIDE and Isabelle/jEdit has 63started in 2008 and was kindly supported by: 64\begin{itemize} 65\item TU M\"unchen \url{http://www.in.tum.de} 66\item BMBF \url{http://www.bmbf.de} 67\item Universit\'e Paris-Sud \url{http://www.u-psud.fr} 68\item Digiteo \url{http://www.digiteo.fr} 69\item ANR \url{http://www.agence-nationale-recherche.fr} 70\end{itemize} 71 72 73\pagenumbering{roman} 74\tableofcontents 75\listoffigures 76\clearfirst 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} 90