# HG changeset patch
# User wenzelm
# Date 936037839 -7200
# Node ID 9228085a25df184dfef5acc70416b2728bf4e044
# Parent  d3f231fe725c25e12f2e4332606b21c067a1bc37
tuned;

diff -r d3f231fe725c -r 9228085a25df doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Mon Aug 30 20:30:21 1999 +0200
+++ b/doc-src/IsarRef/pure.tex	Mon Aug 30 20:30:39 1999 +0200
@@ -769,6 +769,13 @@
 
 \subsection{Block structure}
 
+\indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}}
+\begin{matharray}{rcl}
+  \isarcmd{next} & : & \isartrans{proof(state)}{proof(state)} \\
+  \isarcmd{\{\{} & : & \isartrans{proof(state)}{proof(state)} \\
+  \isarcmd{\}\}} & : & \isartrans{proof(state)}{proof(state)} \\
+\end{matharray}
+
 While Isar is inherently block-structured, opening and closing blocks is
 mostly handled rather casually, with little explicit user-intervention.  Any
 local goal statement automatically opens \emph{two} blocks, which are closed
@@ -782,13 +789,6 @@
 For slightly more advanced applications, there are explicit block parentheses
 as well.  These typically achieve a strong forward style of reasoning.
 
-\indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}}
-\begin{matharray}{rcl}
-  \isarcmd{next} & : & \isartrans{proof(state)}{proof(state)} \\
-  \isarcmd{\{\{} & : & \isartrans{proof(state)}{proof(state)} \\
-  \isarcmd{\}\}} & : & \isartrans{proof(state)}{proof(state)} \\
-\end{matharray}
-
 \begin{descr}
 \item [$\isarkeyword{next}$] switches to a fresh block within a sub-proof,
   resetting the context to the initial one.
@@ -861,8 +861,8 @@
   $\isarkeyword{update_thy}$, and $\isarkeyword{update_thy_only}$] load some
   theory given as $name$ argument.  These commands are exactly the same as the
   corresponding ML functions (see also \cite[\S1,\S6]{isabelle-ref}).  Note
-  that both the ML and Isar versions of these commands may load new- and
-  old-style theories alike.
+  that both the ML and Isar versions may load new- and old-style theories
+  alike.
 \end{descr}
 
 Note that these system commands are scarcely used when working with