removed FIXME: "try_methods" doesn't take a clasimpmod, because it needs to generate Isar proof text in case of success and hence needs total control over its arguments
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri May 27 10:30:08 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri May 27 10:30:08 2011 +0200
@@ -951,8 +951,7 @@
facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? @{syntax thmrefs} ) + ) ? ')'
;
- "} % FIXME try_methods: proper clasimpmod!?
- % FIXME check args "value"
+ "} % FIXME check args "value"
\begin{description}