--- a/doc-src/Ref/Makefile Mon Jun 06 19:08:46 2011 +0200
+++ b/doc-src/Ref/Makefile Mon Jun 06 19:13:48 2011 +0200
@@ -9,10 +9,9 @@
include ../Makefile.in
NAME = ref
-FILES = ref.tex introduction.tex tactic.tex tctical.tex thm.tex \
- defining.tex syntax.tex substitution.tex \
- simplifier.tex classical.tex ../proof.sty ../iman.sty \
- ../extra.sty ../ttbox.sty ../manual.bib
+FILES = ref.tex tactic.tex tctical.tex thm.tex defining.tex syntax.tex \
+ substitution.tex simplifier.tex classical.tex ../proof.sty \
+ ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
dvi: $(NAME).dvi
--- a/doc-src/Ref/introduction.tex Mon Jun 06 19:08:46 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-
-\chapter{Basic Use of Isabelle}
-
-\section{Ending a session}
-\begin{ttbox}
-quit : unit -> unit
-exit : int -> unit
-commit : unit -> bool
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{quit}();] ends the Isabelle session, without saving
- the state.
-
-\item[\ttindexbold{exit} \(i\);] similar to {\tt quit}, passing return
- code \(i\) to the operating system.
-
-\item[\ttindexbold{commit}();] saves the current state without ending
- the session, provided that the logic image is opened read-write;
- return value {\tt false} indicates an error.
-\end{ttdescription}
-
-Typing control-D also finishes the session in essentially the same way
-as the sequence {\tt commit(); quit();} would.
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "ref"
-%%% End:
--- a/doc-src/Ref/ref.tex Mon Jun 06 19:08:46 2011 +0200
+++ b/doc-src/Ref/ref.tex Mon Jun 06 19:13:48 2011 +0200
@@ -47,7 +47,6 @@
\pagenumbering{roman} \tableofcontents \clearfirst
-\include{introduction}
\include{tactic}
\include{tctical}
\include{thm}