--- 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--- 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