a4paper;
authorwenzelm
Tue Oct 12 19:04:25 1999 +0200 (1999-10-12)
changeset 78367a9270282fd3
parent 7835 e9cd3f3be589
child 7837 d4fb2d14edd4
a4paper;
tuned;
doc-src/IsarRef/intro.tex
doc-src/IsarRef/isar-ref.tex
     1.1 --- a/doc-src/IsarRef/intro.tex	Tue Oct 12 18:59:45 1999 +0200
     1.2 +++ b/doc-src/IsarRef/intro.tex	Tue Oct 12 19:04:25 1999 +0200
     1.3 @@ -91,14 +91,24 @@
     1.4  but a good understanding of mathematical proof might cope with Isar even
     1.5  better.
     1.6  
     1.7 -Unfortunately, there is no tutorial on Isabelle/Isar available yet.  This
     1.8 -document really is a \emph{reference manual}.  Nevertheless, we will give some
     1.9 -discussions of the general principles underlying Isar in
    1.10 +This document really is a \emph{reference manual}.  Nevertheless, we will give
    1.11 +some discussions of the general principles underlying Isar in
    1.12  chapter~\ref{ch:basics}, and provide some clues of how these may be put into
    1.13  practice.  Some more background information on Isar is given in
    1.14 -\cite{Wenzel:1999:TPHOL}.  Furthermore, there are several examples distributed
    1.15 -with Isabelle (see directory \texttt{HOL/Isar_examples}).
    1.16 +\cite{Wenzel:1999:TPHOL}.  While there is no proper tutorial on Isabelle/Isar
    1.17 +available yet, there are several examples distributed with Isabelle.  See
    1.18 +\texttt{HOL/Isar_examples} and \texttt{HOL/HOL-Real/HahnBanach} in the
    1.19 +Isabelle library:
    1.20  
    1.21 +\begin{center}\small
    1.22 +  \begin{tabular}{l}
    1.23 +    \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
    1.24 +    \url{http://isabelle.in.tum.de/library/} \\
    1.25 +  \end{tabular}
    1.26 +\end{center}
    1.27 +
    1.28 +Apart from browsable HTML sources, both example sessions also provide actual
    1.29 +documents.
    1.30  
    1.31  %%% Local Variables: 
    1.32  %%% mode: latex
     2.1 --- a/doc-src/IsarRef/isar-ref.tex	Tue Oct 12 18:59:45 1999 +0200
     2.2 +++ b/doc-src/IsarRef/isar-ref.tex	Tue Oct 12 19:04:25 1999 +0200
     2.3 @@ -1,8 +1,8 @@
     2.4  
     2.5  %% $Id$
     2.6  
     2.7 -\documentclass[12pt,fleqn]{report}
     2.8 -\usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../railsetup,../isar,../pdfsetup}
     2.9 +\documentclass[12pt,a4paper,fleqn]{report}
    2.10 +\usepackage{graphicx,../iman,../extra,../proof,../rail,../railsetup,../isar,../pdfsetup}
    2.11  
    2.12  \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
    2.13  \author{\emph{Markus Wenzel} \\ TU M\"unchen}