doc-src/IsarRef/pure.tex

 \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)} \\
+  \BG & : & \isartrans{proof(state)}{proof(state)} \\
+  \EN & : & \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

 
 \section{Other commands}
 
 \subsection{Diagnostics}
 
-\indexisarcmd{typ}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{thm}
-\begin{matharray}{rcl}
-  \isarcmd{typ} & : & \isarkeep{theory~|~proof} \\
+\indexisarcmd{thm}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{typ}
+\begin{matharray}{rcl}
+  \isarcmd{thm} & : & \isarkeep{theory~|~proof} \\
   \isarcmd{term} & : & \isarkeep{theory~|~proof} \\
   \isarcmd{prop} & : & \isarkeep{theory~|~proof} \\
-  \isarcmd{thm} & : & \isarkeep{theory~|~proof} \\
+  \isarcmd{typ} & : & \isarkeep{theory~|~proof} \\
 \end{matharray}
 
 These commands are not part of the actual Isabelle/Isar syntax, but assist
 interactive development.  Also note that $undo$ does not apply here, since the
 theory or proof configuration is not changed.
 
 \begin{rail}
+  'thm' thmrefs
+  ;
+  'term' term
+  ;
+  'prop' prop
+  ;
   'typ' type
   ;
-  'term' term
-  ;
-  'prop' prop
-  ;
-  'thm' thmrefs
-  ;
-\end{rail}
-
-\begin{descr}
-\item [$\isarkeyword{typ}~\tau$] reads and prints types of the meta-logic
-  according to the current theory or proof context.
+\end{rail}
+
+\begin{descr}
+\item [$\isarkeyword{thm}~thms$] retrieves lists of theorems from the current
+  theory or proof context.  Note that any attributes included in the theorem
+  specifications are applied to a temporary context derived from the current
+  theory or proof; the result is discarded, i.e.\ attributes involved in
+  $thms$ do not have any permanent effect.
 \item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, type-checks
   and print terms or propositions according to the current theory or proof
   context; the inferred type of $t$ is output as well.  Note that these
   commands are also useful in inspecting the current environment of term
   abbreviations.
-\item [$\isarkeyword{thm}~thms$] retrieves lists of theorems from the current
-  theory or proof context.  Note that any attributes included in the theorem
-  specifications are applied to a temporary context derived from the current
-  theory or proof; the result is discarded, i.e.\ attributes involved in
-  $thms$ do not have any permanent effect.
+\item [$\isarkeyword{typ}~\tau$] reads and prints types of the meta-logic
+  according to the current theory or proof context.
 \end{descr}
 
 
 \subsection{System operations}