diff -r 0e70a29d3e02 -r 97ba7a7651de doc-src/IsarRef/Thy/Misc.thy --- 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