doc-src/IsarRef/pure.tex
changeset 8896 c80aba8c1d5e
parent 8883 2a94bfd31285
child 8946 40e06237934c
     1.1 --- a/doc-src/IsarRef/pure.tex	Sun May 21 14:32:47 2000 +0200
     1.2 +++ b/doc-src/IsarRef/pure.tex	Sun May 21 14:33:46 2000 +0200
     1.3 @@ -911,7 +911,7 @@
     1.4  
     1.5  \subsection{Block structure}
     1.6  
     1.7 -\indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}}
     1.8 +\indexisarcmd{next}\indexisarcmd{\{}\indexisarcmd{\}}
     1.9  \begin{matharray}{rcl}
    1.10    \NEXT & : & \isartrans{proof(state)}{proof(state)} \\
    1.11    \BG & : & \isartrans{proof(state)}{proof(state)} \\
    1.12 @@ -933,9 +933,8 @@
    1.13  \begin{descr}
    1.14  \item [$\NEXT$] switches to a fresh block within a sub-proof, resetting the
    1.15    local context to the initial one.
    1.16 -\item [$\isarkeyword{\{\{}$ and $\isarkeyword{\}\}}$] explicitly open and
    1.17 -  close blocks.  Any current facts pass through ``$\isarkeyword{\{\{}$''
    1.18 -  unchanged, while ``$\isarkeyword{\}\}}$'' causes any result to be
    1.19 +\item [$\BG$ and $\EN$] explicitly open and close blocks.  Any current facts
    1.20 +  pass through ``$\BG$'' unchanged, while ``$\EN$'' causes any result to be
    1.21    \emph{exported} into the enclosing context.  Thus fixed variables are
    1.22    generalized, assumptions discharged, and local definitions unfolded (cf.\ 
    1.23    \S\ref{sec:proof-context}).  There is no difference of $\ASSUMENAME$ and