author wenzelm Wed, 31 Jul 2013 23:41:32 +0200 changeset 52820 cb53b44b958c parent 52819 7ce3ebc268a1 child 52821 05eb2d77b195
recovered "\<phi>\<^isub>i" from 0b02aaf7c7c5;
```--- a/src/Doc/IsarImplementation/Tactic.thy	Wed Jul 31 22:15:17 2013 +0200
+++ b/src/Doc/IsarImplementation/Tactic.thy	Wed Jul 31 23:41:32 2013 +0200
@@ -509,7 +509,7 @@
regarded as an atomic formula, to solve premise @{text "i"} of
@{text "thm\<^sub>2"}.  Let @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} be @{text
"\<psi>"} and @{text "\<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>"}.  The unique @{text "s"} that
-  unifies @{text "\<psi>"} and @{text "\<phi>"} yields the theorem @{text "(\<phi>\<^sub>1 \<Longrightarrow>
+  unifies @{text "\<psi>"} and @{text "\<phi>\<^isub>i"} yields the theorem @{text "(\<phi>\<^sub>1 \<Longrightarrow>
\<dots> \<phi>\<^sub>i\<^sub>-\<^sub>1 \<Longrightarrow> \<phi>\<^sub>i\<^sub>+\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>)s"}.  Multiple results are considered as
error (exception @{ML THM}).
```