# HG changeset patch # User blanchet # Date 1306485008 -7200 # Node ID 619f16bf2150611f0d0f5540567255587ad048fb # Parent 121aa59b4d174051763e051639885953f4dbc066 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 diff -r 121aa59b4d17 -r 619f16bf2150 doc-src/IsarRef/Thy/HOL_Specific.thy --- 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}