--- a/src/Doc/Implementation/Logic.thy Tue Dec 29 17:54:45 2015 +0100
+++ b/src/Doc/Implementation/Logic.thy Tue Dec 29 19:11:23 2015 +0100
@@ -1011,7 +1011,7 @@
(again modulo unification):
\[
\infer[(@{inference_def assumption})]{\<open>C\<vartheta>\<close>}
- {\<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C\<close> & \<open>A\<vartheta> = H\<^sub>i\<vartheta>\<close>~~\text{(for some~\<open>i\<close>)}}
+ {\<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C\<close> & \<open>A\<vartheta> = H\<^sub>i\<vartheta>\<close>~~\mbox{(for some~\<open>i\<close>)}}
\]
%FIXME @{inference_def elim_resolution}, @{inference_def dest_resolution}