src/Doc/JEdit/document/root.tex
author wenzelm
Thu, 10 Oct 2013 12:02:12 +0200
changeset 54320 b8bd31c7058c
parent 53776 3806bf1d2a33
child 54356 9538f51da542
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
53769
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
     1
\documentclass[12pt,a4paper]{report}
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
     2
\usepackage{supertabular}
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
     3
\usepackage{graphicx}
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
     4
\usepackage{iman,extra,isar,ttbox}
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
     5
\usepackage[nohyphen,strings]{underscore}
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
     6
\usepackage{isabelle,isabellesym}
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
     7
\usepackage{railsetup}
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
     8
\usepackage{style}
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
     9
\usepackage{pdfsetup}
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    10
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    11
\hyphenation{Isabelle}
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    12
\hyphenation{Isar}
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    13
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    14
\isadroptag{theory}
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    15
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    16
\isabellestyle{literal}
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    17
53775
ab1ae01b41bc clarified logo;
wenzelm
parents: 53771
diff changeset
    18
\title{\includegraphics[scale=0.5]{isabelle_jedit} \\[4ex] Isabelle/jEdit}
53769
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    19
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    20
\author{\emph{Makarius Wenzel}}
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    21
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    22
\makeindex
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    23
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    24
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    25
\begin{document}
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    26
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    27
\maketitle
53770
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
    28
53776
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    29
\begin{abstract}
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    30
  Isabelle/jEdit is a fully-featured Prover IDE, based on Isabelle/Scala and
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    31
  the jEdit text editor. This document provides an overview of general
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    32
  principles and its main IDE functionality.
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    33
\end{abstract}
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    34
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    35
\vspace*{2.5cm}
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    36
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    37
\begin{quote}
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    38
  {\small\em Isabelle's user interface is no advance over LCF's, which is
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    39
  widely condemned as ``user-unfriendly'': hard to use, bewildering to
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    40
  beginners. Hence the interest in proof editors, where a proof can be
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    41
  constructed and modified rule-by-rule using windows, mouse, and menus. But
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    42
  Edinburgh LCF was invented because real proofs require millions of
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    43
  inferences. Sophisticated tools --- rules, tactics and tacticals, the
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    44
  language ML, the logics themselves --- are hard to learn, yet they are
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    45
  essential. We may demand a mouse, but we need better education and
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    46
  training.}
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    47
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    48
  Lawrence C. Paulson, ``Isabelle: The Next 700 Theorem Provers''
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    49
\end{quote}
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    50
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    51
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    52
\vspace*{2.5cm}
3806bf1d2a33 more front-matter;
wenzelm
parents: 53775
diff changeset
    53
53770
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
    54
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
    55
\subsubsection*{Acknowledgements}
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
    56
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
    57
Research and implementation of concepts around PIDE and Isabelle/jEdit has
53771
wenzelm
parents: 53770
diff changeset
    58
started around 2008 and was kindly supported by:
53770
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
    59
\begin{itemize}
54320
wenzelm
parents: 53776
diff changeset
    60
\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
    61
\item BMBF \url{http://www.bmbf.de}
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
    62
\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
    63
\item Digiteo \url{http://www.digiteo.fr}
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
    64
\item ANR \url{http://www.agence-nationale-recherche.fr}
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
    65
\end{itemize}
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
    66
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
    67
53769
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    68
\pagenumbering{roman} \tableofcontents \clearfirst
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    69
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    70
\input{JEdit.tex}
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    71
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    72
\begingroup
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    73
  \tocentry{\bibname}
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    74
  \bibliographystyle{abbrv} \small\raggedright\frenchspacing
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    75
  \bibliography{manual}
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    76
\endgroup
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    77
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    78
\tocentry{\indexname}
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    79
\printindex
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    80
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    81
\end{document}