# HG changeset patch
# User wenzelm
# Date 1157393275 -7200
# Node ID a04bf731ceb64f132a18f2d2932b46f161993802
# Parent  af069653f1d7516355ab5cbd7e1836e0f4189bb4
tuned;

diff -r af069653f1d7 -r a04bf731ceb6 doc-src/IsarImplementation/Thy/document/integration.tex
--- a/doc-src/IsarImplementation/Thy/document/integration.tex	Mon Sep 04 19:49:39 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex	Mon Sep 04 20:07:55 2006 +0200
@@ -150,10 +150,10 @@
 
   The operational part is represented as the sequential union of a
   list of partial functions, which are tried in turn until the first
-  one succeeds (i.e.\ does not raise \verb|Toplevel.UNDEF|).  This acts
-  like an outer case-expression for various alternative state
-  transitions.  For example, \isakeyword{qed} acts differently for a
-  local proofs vs.\ the global ending of the main proof.
+  one succeeds.  This acts like an outer case-expression for various
+  alternative state transitions.  For example, \isakeyword{qed} acts
+  differently for a local proofs vs.\ the global ending of the main
+  proof.
 
   Toplevel transitions are composed via transition transformers.
   Internally, Isar commands are put together from an empty transition
@@ -274,9 +274,9 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-The {\ML} toplevel provides a read-compile-eval-print loop for
-  {\ML} values, types, structures, and functors.  {\ML} declarations
-  operate on the global system state, which consists of the compiler
+The {\ML} toplevel provides a read-compile-eval-print loop for {\ML}
+  values, types, structures, and functors.  {\ML} declarations operate
+  on the global system state, which consists of the compiler
   environment plus the values of {\ML} reference variables.  There is
   no clean way to undo {\ML} declarations, except for reverting to a
   previously saved state of the whole Isabelle process.  {\ML} input
diff -r af069653f1d7 -r a04bf731ceb6 doc-src/IsarImplementation/Thy/document/prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/prelim.tex	Mon Sep 04 19:49:39 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex	Mon Sep 04 20:07:55 2006 +0200
@@ -477,6 +477,12 @@
 }
 \isamarkuptrue%
 %
+\isadelimFIXME
+%
+\endisadelimFIXME
+%
+\isatagFIXME
+%
 \begin{isamarkuptext}%
 FIXME tune
 
@@ -511,10 +517,23 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\endisatagFIXME
+{\isafoldFIXME}%
+%
+\isadelimFIXME
+%
+\endisadelimFIXME
+%
 \isamarkupsubsection{Strings of symbols%
 }
 \isamarkuptrue%
 %
+\isadelimFIXME
+%
+\endisadelimFIXME
+%
+\isatagFIXME
+%
 \begin{isamarkuptext}%
 FIXME tune
 
@@ -565,6 +584,13 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\endisatagFIXME
+{\isafoldFIXME}%
+%
+\isadelimFIXME
+%
+\endisadelimFIXME
+%
 \isadelimmlref
 %
 \endisadelimmlref
@@ -620,6 +646,12 @@
 }
 \isamarkuptrue%
 %
+\isadelimFIXME
+%
+\endisadelimFIXME
+%
+\isatagFIXME
+%
 \begin{isamarkuptext}%
 FIXME tune
 
@@ -642,6 +674,13 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\endisatagFIXME
+{\isafoldFIXME}%
+%
+\isadelimFIXME
+%
+\endisadelimFIXME
+%
 \isadelimmlref
 %
 \endisadelimmlref
diff -r af069653f1d7 -r a04bf731ceb6 doc-src/IsarImplementation/Thy/integration.thy
--- a/doc-src/IsarImplementation/Thy/integration.thy	Mon Sep 04 19:49:39 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/integration.thy	Mon Sep 04 20:07:55 2006 +0200
@@ -114,10 +114,10 @@
 
   The operational part is represented as the sequential union of a
   list of partial functions, which are tried in turn until the first
-  one succeeds (i.e.\ does not raise @{ML Toplevel.UNDEF}).  This acts
-  like an outer case-expression for various alternative state
-  transitions.  For example, \isakeyword{qed} acts differently for a
-  local proofs vs.\ the global ending of the main proof.
+  one succeeds.  This acts like an outer case-expression for various
+  alternative state transitions.  For example, \isakeyword{qed} acts
+  differently for a local proofs vs.\ the global ending of the main
+  proof.
 
   Toplevel transitions are composed via transition transformers.
   Internally, Isar commands are put together from an empty transition
@@ -219,9 +219,10 @@
 
 section {* ML toplevel \label{sec:ML-toplevel} *}
 
-text {* The {\ML} toplevel provides a read-compile-eval-print loop for
-  {\ML} values, types, structures, and functors.  {\ML} declarations
-  operate on the global system state, which consists of the compiler
+text {*
+  The {\ML} toplevel provides a read-compile-eval-print loop for {\ML}
+  values, types, structures, and functors.  {\ML} declarations operate
+  on the global system state, which consists of the compiler
   environment plus the values of {\ML} reference variables.  There is
   no clean way to undo {\ML} declarations, except for reverting to a
   previously saved state of the whole Isabelle process.  {\ML} input
diff -r af069653f1d7 -r a04bf731ceb6 doc-src/IsarImplementation/Thy/prelim.thy
--- a/doc-src/IsarImplementation/Thy/prelim.thy	Mon Sep 04 19:49:39 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/prelim.thy	Mon Sep 04 20:07:55 2006 +0200
@@ -405,7 +405,7 @@
 
 section {* Name spaces *}
 
-text {*
+text %FIXME {*
   FIXME tune
 
   By general convention, each kind of formal entities (logical
@@ -444,7 +444,7 @@
 
 subsection {* Strings of symbols *}
 
-text {*
+text %FIXME {*
   FIXME tune
 
   Isabelle strings consist of a sequence of
@@ -542,7 +542,7 @@
 
 subsection {* Qualified names *}
 
-text {*
+text %FIXME {*
   FIXME tune
 
   A \emph{qualified name} essentially consists of a non-empty list of
diff -r af069653f1d7 -r a04bf731ceb6 doc-src/IsarImplementation/implementation.tex
--- a/doc-src/IsarImplementation/implementation.tex	Mon Sep 04 19:49:39 2006 +0200
+++ b/doc-src/IsarImplementation/implementation.tex	Mon Sep 04 20:07:55 2006 +0200
@@ -18,7 +18,9 @@
   \\[4ex] The Isabelle/Isar Implementation}
 \author{\emph{Makarius Wenzel}}
 
-\makeglossary
+%FIXME
+%\makeglossary
+
 \makeindex
 
 
@@ -78,8 +80,9 @@
 \bibliography{../manual}
 \endgroup
 
-\tocentry{\glossaryname}
-\printglossary
+%FIXME
+%\tocentry{\glossaryname}
+%\printglossary
 
 \tocentry{\indexname}
 \printindex