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
authorblanchet
Fri, 27 May 2011 10:30:08 +0200
changeset 43019 619f16bf2150
parent 43018 121aa59b4d17
child 43020 abb5d1f907e4
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
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}