# HG changeset patch
# User wenzelm
# Date 1307380428 -7200
# Node ID e68c3861b8db3dfe873858129c0099bd4027f9b8
# Parent  287182c2f23a980244acdd5c49d42e1c27d59ac1
removed odd remains of low-level session management;

diff -r 287182c2f23a -r e68c3861b8db doc-src/Ref/Makefile
--- 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
 
diff -r 287182c2f23a -r e68c3861b8db doc-src/Ref/introduction.tex
--- 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: 
diff -r 287182c2f23a -r e68c3861b8db doc-src/Ref/ref.tex
--- 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}