# HG changeset patch
# User kleing
# Date 1234520070 -39600
# Node ID 97ba7a7651dec11c0f57ecbf9d772590b340141a
# Parent  0e70a29d3e029b22d1088c4509a1f63e343facde
typo

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
diff -r 0e70a29d3e02 -r 97ba7a7651de doc-src/IsarRef/Thy/document/Misc.tex
--- a/doc-src/IsarRef/Thy/document/Misc.tex	Fri Feb 13 16:00:45 2009 +1100
+++ b/doc-src/IsarRef/Thy/document/Misc.tex	Fri Feb 13 21:14:30 2009 +1100
@@ -51,7 +51,7 @@
     thmcriterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
       'solves' | 'simp' ':' term | term)
     ;
-    'find\_consts' (constcriterion +)
+    'find\_consts' (constcriterion *)
     ;
     constcriterion: ('-'?) ('name' ':' nameref | 'strict' ':' type | type)
     ;
@@ -88,7 +88,7 @@
   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 criteria \isa{{\isachardoublequote}solves{\isachardoublequote}} returns all rules
+  respectively.  The criterion \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