# HG changeset patch
# User wenzelm
# Date 1484929374 -3600
# Node ID 75ee8475c37e87390c58bc53faa90f45628172a7
# Parent  5eda897876213430b454e0d4bb29d0cb74d61f8f
tuned;

diff -r 5eda89787621 -r 75ee8475c37e src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Fri Jan 20 12:44:44 2017 +0100
+++ b/src/Doc/Isar_Ref/Proof.thy	Fri Jan 20 17:22:54 2017 +0100
@@ -16,10 +16,10 @@
     \<^descr> \<open>proof(prove)\<close> means that a new goal has just been stated that is now to
     be \<^emph>\<open>proven\<close>; the next command may refine it by some proof method, and
     enter a sub-proof to establish the actual result.
-  
+
     \<^descr> \<open>proof(state)\<close> is like a nested theory mode: the context may be
     augmented by \<^emph>\<open>stating\<close> additional assumptions, intermediate results etc.
-  
+
     \<^descr> \<open>proof(chain)\<close> is intermediate between \<open>proof(state)\<close> and
     \<open>proof(prove)\<close>: existing facts (i.e.\ the contents of the special
     @{fact_ref this} register) have been just picked up in order to be used
@@ -544,7 +544,7 @@
 
   \begin{matharray}{rcl}
     @{command "also"}\<open>\<^sub>0\<close> & \equiv & @{command "note"}~\<open>calculation = this\<close> \\
-    @{command "also"}\<open>\<^sub>n+1\<close> & \equiv & @{command "note"}~\<open>calculation = trans [OF calculation this]\<close> \\[0.5ex]
+    @{command "also"}\<open>\<^sub>n\<^sub>+\<^sub>1\<close> & \equiv & @{command "note"}~\<open>calculation = trans [OF calculation this]\<close> \\[0.5ex]
     @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~\<open>calculation\<close> \\[0.5ex]
     @{command "moreover"} & \equiv & @{command "note"}~\<open>calculation = calculation this\<close> \\
     @{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~\<open>calculation\<close> \\
@@ -565,10 +565,10 @@
   from the current context, unless alternative rules are given as explicit
   arguments.
 
-  \<^descr> @{command "finally"}~\<open>(a\<^sub>1 \<dots> a\<^sub>n)\<close> maintaining @{fact calculation} in the
-  same way as @{command "also"}, and concludes the current calculational
+  \<^descr> @{command "finally"}~\<open>(a\<^sub>1 \<dots> a\<^sub>n)\<close> maintains @{fact calculation} in the
+  same way as @{command "also"} and then concludes the current calculational
   thread. The final result is exhibited as fact for forward chaining towards
-  the next goal. Basically, @{command "finally"} just abbreviates @{command
+  the next goal. Basically, @{command "finally"} abbreviates @{command
   "also"}~@{command "from"}~@{fact calculation}. Typical idioms for concluding
   calculational proofs are ``@{command "finally"}~@{command
   "show"}~\<open>?thesis\<close>~@{command "."}'' and ``@{command "finally"}~@{command
@@ -678,7 +678,7 @@
     newly stated goal to a number of sub-goals that are to be solved later.
     Facts are passed to \<open>m\<^sub>1\<close> for forward chaining, if so indicated by
     \<open>proof(chain)\<close> mode.
-  
+
     \<^enum> A \<^emph>\<open>terminal\<close> conclusion step @{command_ref "qed"}~\<open>m\<^sub>2\<close> is intended to
     solve remaining goals. No facts are passed to \<open>m\<^sub>2\<close>.