61 criteria. The criterion @{text "name: p"} selects all theorems |
61 criteria. The criterion @{text "name: p"} selects all theorems |
62 whose fully qualified name matches pattern @{text p}, which may |
62 whose fully qualified name matches pattern @{text p}, which may |
63 contain ``@{text "*"}'' wildcards. The criteria @{text intro}, |
63 contain ``@{text "*"}'' wildcards. The criteria @{text intro}, |
64 @{text elim}, and @{text dest} select theorems that match the |
64 @{text elim}, and @{text dest} select theorems that match the |
65 current goal as introduction, elimination or destruction rules, |
65 current goal as introduction, elimination or destruction rules, |
66 respectively. The criterion @{text "simp: t"} selects all rewrite |
66 respectively. The criteria @{text "solves"} returns all rules |
67 rules whose left-hand side matches the given term. The criterion |
67 that would directly solve the current goal. The criterion |
68 term @{text t} selects all theorems that contain the pattern @{text |
68 @{text "simp: t"} selects all rewrite rules whose left-hand side |
69 t} -- as usual, patterns may contain occurrences of the dummy |
69 matches the given term. The criterion term @{text t} selects all |
70 ``@{text _}'', schematic variables, and type constraints. |
70 theorems that contain the pattern @{text t} -- as usual, patterns |
|
71 may contain occurrences of the dummy ``@{text _}'', schematic |
|
72 variables, and type constraints. |
71 |
73 |
72 Criteria can be preceded by ``@{text "-"}'' to select theorems that |
74 Criteria can be preceded by ``@{text "-"}'' to select theorems that |
73 do \emph{not} match. Note that giving the empty list of criteria |
75 do \emph{not} match. Note that giving the empty list of criteria |
74 yields \emph{all} currently known facts. An optional limit for the |
76 yields \emph{all} currently known facts. An optional limit for the |
75 number of printed facts may be given; the default is 40. By |
77 number of printed facts may be given; the default is 40. By |