# HG changeset patch
# User wenzelm
# Date 1436190308 -7200
# Node ID 61be352b1f79924daedf93f0c18931404a953ad5
# Parent  263a8f15faf3844f79b6b5fb31b3b3eaeafa5325
tuned;

diff -r 263a8f15faf3 -r 61be352b1f79 src/Doc/Isar_Ref/Misc.thy
--- a/src/Doc/Isar_Ref/Misc.thy	Mon Jul 06 15:34:45 2015 +0200
+++ b/src/Doc/Isar_Ref/Misc.thy	Mon Jul 06 15:45:08 2015 +0200
@@ -27,14 +27,14 @@
       @@{command print_theorems} |
       @@{command print_facts}) ('!'?)
     ;
-    @@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \<newline> (thmcriterion * )
+    @@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \<newline> (thm_criterion*)
     ;
-    thmcriterion: ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' |
+    thm_criterion: ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' |
       'solves' | 'simp' ':' @{syntax term} | @{syntax term})
     ;
-    @@{command find_consts} (constcriterion * )
+    @@{command find_consts} (const_criterion*)
     ;
-    constcriterion: ('-'?)
+    const_criterion: ('-'?)
       ('name' ':' @{syntax nameref} | 'strict' ':' @{syntax type} | @{syntax type})
     ;
     @@{command thm_deps} @{syntax thmrefs}