--- 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%
%
--- 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%
%
--- 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%
%
--- 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
--- 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
--- 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