--- a/src/Doc/IsarImplementation/Logic.thy Fri Jun 21 13:36:10 2013 +0200
+++ b/src/Doc/IsarImplementation/Logic.thy Sat Jun 22 18:24:06 2013 +0200
@@ -1148,7 +1148,7 @@
{@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C"} & @{text "A\<vartheta> = H\<^sub>i\<vartheta>"}~~\text{(for some~@{text i})}}
\]
- FIXME @{inference_def elim_resolution}, @{inference_def dest_resolution}
+ %FIXME @{inference_def elim_resolution}, @{inference_def dest_resolution}
*}
text %mlref {*