# HG changeset patch
# User wenzelm
# Date 1157058076 -7200
# Node ID 6d8b29c7a960fcb2cce220d93214d55204a0b451
# Parent  27ea2ba48fa3071206761171b77abdcfcc1d705c
tuned;

diff -r 27ea2ba48fa3 -r 6d8b29c7a960 doc-src/IsarImplementation/Thy/document/prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/prelim.tex	Thu Aug 31 22:55:49 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex	Thu Aug 31 23:01:16 2006 +0200
@@ -473,7 +473,7 @@
 %
 \endisadelimmlref
 %
-\isamarkupsection{Named entities%
+\isamarkupsection{Name spaces%
 }
 \isamarkuptrue%
 %
@@ -612,7 +612,7 @@
 %
 \endisadelimmlref
 %
-\isamarkupsubsection{Qualified names and name spaces%
+\isamarkupsubsection{Qualified names%
 }
 \isamarkuptrue%
 %
diff -r 27ea2ba48fa3 -r 6d8b29c7a960 doc-src/IsarImplementation/Thy/document/proof.tex
--- a/doc-src/IsarImplementation/Thy/document/proof.tex	Thu Aug 31 22:55:49 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex	Thu Aug 31 23:01:16 2006 +0200
@@ -23,7 +23,7 @@
 }
 \isamarkuptrue%
 %
-\isamarkupsection{Local variables%
+\isamarkupsection{Variables and schematic polymorphism%
 }
 \isamarkuptrue%
 %
@@ -101,15 +101,6 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Schematic polymorphism%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
 \isamarkupsection{Assumptions%
 }
 \isamarkuptrue%
@@ -128,7 +119,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Structured proofs \label{sec:isar-proof-state}%
+\isamarkupsection{Proof states \label{sec:isar-proof-state}%
 }
 \isamarkuptrue%
 %
diff -r 27ea2ba48fa3 -r 6d8b29c7a960 doc-src/IsarImplementation/Thy/document/tactic.tex
--- a/doc-src/IsarImplementation/Thy/document/tactic.tex	Thu Aug 31 22:55:49 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/tactic.tex	Thu Aug 31 23:01:16 2006 +0200
@@ -19,7 +19,7 @@
 %
 \endisadelimtheory
 %
-\isamarkupchapter{Goal-directed reasoning%
+\isamarkupchapter{Tactical reasoning%
 }
 \isamarkuptrue%
 %
diff -r 27ea2ba48fa3 -r 6d8b29c7a960 doc-src/IsarImplementation/Thy/prelim.thy
--- a/doc-src/IsarImplementation/Thy/prelim.thy	Thu Aug 31 22:55:49 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/prelim.thy	Thu Aug 31 23:01:16 2006 +0200
@@ -403,7 +403,7 @@
 *}
 
 
-section {* Named entities *}
+section {* Name spaces *}
 
 text {*
   By general convention, each kind of formal entities (logical
@@ -536,7 +536,7 @@
 *}
 
 
-subsection {* Qualified names and name spaces *}
+subsection {* Qualified names *}
 
 text {*
   A \emph{qualified name} essentially consists of a non-empty list of
diff -r 27ea2ba48fa3 -r 6d8b29c7a960 doc-src/IsarImplementation/Thy/proof.thy
--- a/doc-src/IsarImplementation/Thy/proof.thy	Thu Aug 31 22:55:49 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/proof.thy	Thu Aug 31 23:01:16 2006 +0200
@@ -5,7 +5,7 @@
 
 chapter {* Structured proofs *}
 
-section {* Local variables *}
+section {* Variables and schematic polymorphism *}
 
 text FIXME
 
@@ -65,11 +65,6 @@
 text FIXME
 
 
-section {* Schematic polymorphism *}
-
-text FIXME
-
-
 section {* Assumptions *}
 
 text FIXME
@@ -80,7 +75,7 @@
 text FIXME
 
 
-section {* Structured proofs \label{sec:isar-proof-state} *}
+section {* Proof states \label{sec:isar-proof-state} *}
 
 text {*
   FIXME
diff -r 27ea2ba48fa3 -r 6d8b29c7a960 doc-src/IsarImplementation/Thy/tactic.thy
--- a/doc-src/IsarImplementation/Thy/tactic.thy	Thu Aug 31 22:55:49 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/tactic.thy	Thu Aug 31 23:01:16 2006 +0200
@@ -3,7 +3,7 @@
 
 theory tactic imports base begin
 
-chapter {* Goal-directed reasoning *}
+chapter {* Tactical reasoning *}
 
 text {*
   The basic idea of tactical theorem proving is to refine the initial