diff -r ffb153ef6366 -r 76d7f6c9a14c doc-src/TutorialI/Advanced/document/Partial.tex
--- a/doc-src/TutorialI/Advanced/document/Partial.tex	Mon Dec 18 16:11:53 2000 +0100
+++ b/doc-src/TutorialI/Advanced/document/Partial.tex	Mon Dec 18 16:45:17 2000 +0100
@@ -173,12 +173,10 @@
 \isa{while{\isacharunderscore}rule}, the well known proof rule for total
 correctness of loops expressed with \isa{while}:
 \begin{isabelle}%
-\ \ \ \ \ P\ s\ {\isasymLongrightarrow}\isanewline
-\ \ \ \ \ {\isacharparenleft}{\isasymAnd}s{\isachardot}\ P\ s\ {\isasymLongrightarrow}\ b\ s\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}c\ s{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
-\ \ \ \ \ {\isacharparenleft}{\isasymAnd}s{\isachardot}\ P\ s\ {\isasymLongrightarrow}\ {\isasymnot}\ b\ s\ {\isasymLongrightarrow}\ Q\ s{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
-\ \ \ \ \ wf\ r\ {\isasymLongrightarrow}\isanewline
-\ \ \ \ \ {\isacharparenleft}{\isasymAnd}s{\isachardot}\ P\ s\ {\isasymLongrightarrow}\ b\ s\ {\isasymLongrightarrow}\ {\isacharparenleft}c\ s{\isacharcomma}\ s{\isacharparenright}\ {\isasymin}\ r{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
-\ \ \ \ \ Q\ {\isacharparenleft}while\ b\ c\ s{\isacharparenright}%
+\ \ \ \ \ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}c\ s{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ \ \ \ \ \ \ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymnot}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ Q\ s{\isacharsemicolon}\ wf\ r{\isacharsemicolon}\isanewline
+\ \ \ \ \ \ \ \ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}c\ s{\isacharcomma}\ s{\isacharparenright}\ {\isasymin}\ r{\isasymrbrakk}\isanewline
+\ \ \ \ \ {\isasymLongrightarrow}\ Q\ {\isacharparenleft}while\ b\ c\ s{\isacharparenright}%
 \end{isabelle} \isa{P} needs to be
 true of the initial state \isa{s} and invariant under \isa{c}
 (premises 1 and 2).The post-condition \isa{Q} must become true when