# HG changeset patch
# User kleing
# Date 1234486142 -39600
# Node ID defab1c6a6b541e495fb357af41f747623c0280e
# Parent  4a396c7a77b5cd447f78d52e935787f1a82612a5
FindTheorems solves: update documentation (by Timothy Bourke)

diff -r 4a396c7a77b5 -r defab1c6a6b5 doc-src/IsarRef/Thy/Misc.thy
--- a/doc-src/IsarRef/Thy/Misc.thy	Fri Feb 13 10:41:56 2009 +0100
+++ b/doc-src/IsarRef/Thy/Misc.thy	Fri Feb 13 11:49:02 2009 +1100
@@ -28,7 +28,7 @@
     'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *)
     ;
     criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
-      'simp' ':' term | term)
+      'solves' | 'simp' ':' term | term)
     ;
     'thm\_deps' thmrefs
     ;
@@ -63,11 +63,13 @@
   contain ``@{text "*"}'' wildcards.  The criteria @{text intro},
   @{text elim}, and @{text dest} select theorems that match the
   current goal as introduction, elimination or destruction rules,
-  respectively.  The criterion @{text "simp: t"} selects all rewrite
-  rules whose left-hand side matches the given term.  The criterion
-  term @{text t} selects all theorems that contain the pattern @{text
-  t} -- as usual, patterns may contain occurrences of the dummy
-  ``@{text _}'', schematic variables, and type constraints.
+  respectively.  The criteria @{text "solves"} returns all rules
+  that would directly solve the current goal.  The criterion
+  @{text "simp: t"} selects all rewrite rules whose left-hand side
+  matches the given term.  The criterion term @{text t} selects all
+  theorems that contain the pattern @{text t} -- as usual, patterns
+  may contain occurrences of the dummy ``@{text _}'', schematic
+  variables, and type constraints.
   
   Criteria can be preceded by ``@{text "-"}'' to select theorems that
   do \emph{not} match. Note that giving the empty list of criteria
diff -r 4a396c7a77b5 -r defab1c6a6b5 doc-src/IsarRef/Thy/document/Misc.tex
--- a/doc-src/IsarRef/Thy/document/Misc.tex	Fri Feb 13 10:41:56 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Misc.tex	Fri Feb 13 11:49:02 2009 +1100
@@ -48,7 +48,7 @@
     'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *)
     ;
     criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
-      'simp' ':' term | term)
+      'solves' | 'simp' ':' term | term)
     ;
     'thm\_deps' thmrefs
     ;
@@ -83,10 +83,13 @@
   contain ``\isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}'' wildcards.  The criteria \isa{intro},
   \isa{elim}, and \isa{dest} select theorems that match the
   current goal as introduction, elimination or destruction rules,
-  respectively.  The criterion \isa{{\isachardoublequote}simp{\isacharcolon}\ t{\isachardoublequote}} selects all rewrite
-  rules whose left-hand side matches the given term.  The criterion
-  term \isa{t} selects all theorems that contain the pattern \isa{t} -- as usual, patterns may contain occurrences of the dummy
-  ``\isa{{\isacharunderscore}}'', schematic variables, and type constraints.
+  respectively.  The criteria \isa{{\isachardoublequote}solves{\isachardoublequote}} returns all rules
+  that would directly solve the current goal.  The criterion
+  \isa{{\isachardoublequote}simp{\isacharcolon}\ t{\isachardoublequote}} selects all rewrite rules whose left-hand side
+  matches the given term.  The criterion term \isa{t} selects all
+  theorems that contain the pattern \isa{t} -- as usual, patterns
+  may contain occurrences of the dummy ``\isa{{\isacharunderscore}}'', schematic
+  variables, and type constraints.
   
   Criteria can be preceded by ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' to select theorems that
   do \emph{not} match. Note that giving the empty list of criteria