--- a/doc-src/IsarRef/Thy/Misc.thy Fri Feb 13 16:00:45 2009 +1100
+++ b/doc-src/IsarRef/Thy/Misc.thy Fri Feb 13 21:14:30 2009 +1100
@@ -68,7 +68,7 @@
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 criteria @{text "solves"} returns all rules
+ respectively. The criterion @{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