# HG changeset patch
# User kleing
# Date 1234497445 -39600
# Node ID e0e3aa62d9d37c6b50b0a1ec92e16f6c3b3f372a
# Parent  defab1c6a6b541e495fb357af41f747623c0280e
find_consts: documentation. (by Timothy Bourke)

diff -r defab1c6a6b5 -r e0e3aa62d9d3 doc-src/IsarRef/Thy/Misc.thy
--- a/doc-src/IsarRef/Thy/Misc.thy	Fri Feb 13 11:49:02 2009 +1100
+++ b/doc-src/IsarRef/Thy/Misc.thy	Fri Feb 13 14:57:25 2009 +1100
@@ -16,6 +16,7 @@
     @{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def "print_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def "find_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+    @{command_def "find_consts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def "thm_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@@ -25,11 +26,15 @@
     'print\_theory' ( '!'?)
     ;
 
-    'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *)
+    'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (thmcriterion *)
     ;
-    criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
+    thmcriterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
       'solves' | 'simp' ':' term | term)
     ;
+    'find\_consts' (constcriterion *)
+    ;
+    constcriterion: ('-'?) ('name' ':' nameref | 'strict' ':' type | type)
+    ;
     'thm\_deps' thmrefs
     ;
   \end{rail}
@@ -77,7 +82,16 @@
   number of printed facts may be given; the default is 40.  By
   default, duplicates are removed from the search result. Use
   @{text with_dups} to display duplicates.
-  
+
+  \item @{command "find_consts"}~@{text criteria} prints all constants
+  whose type meets all of the given criteria. The criterion @{text
+  "strict: ty"} is met by any type that matches the type pattern
+  @{text ty}.  Patterns may contain both the dummy type ``@{text _}''
+  and sort constraints. The criterion @{text ty} is similar, but it
+  also matches against subtypes. The criterion @{text "name: p"} and
+  the prefix ``@{text "-"}'' function as described for @{command
+  "find_theorems"}.
+
   \item @{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}
   visualizes dependencies of facts, using Isabelle's graph browser
   tool (see also \cite{isabelle-sys}).
diff -r defab1c6a6b5 -r e0e3aa62d9d3 doc-src/IsarRef/Thy/document/Misc.tex
--- a/doc-src/IsarRef/Thy/document/Misc.tex	Fri Feb 13 11:49:02 2009 +1100
+++ b/doc-src/IsarRef/Thy/document/Misc.tex	Fri Feb 13 14:57:25 2009 +1100
@@ -36,6 +36,7 @@
     \indexdef{}{command}{print\_attributes}\hypertarget{command.print-attributes}{\hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
     \indexdef{}{command}{print\_theorems}\hypertarget{command.print-theorems}{\hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
     \indexdef{}{command}{find\_theorems}\hypertarget{command.find-theorems}{\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
+    \indexdef{}{command}{find\_consts}\hypertarget{command.find-consts}{\hyperlink{command.find-consts}{\mbox{\isa{\isacommand{find{\isacharunderscore}consts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
     \indexdef{}{command}{thm\_deps}\hypertarget{command.thm-deps}{\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
     \indexdef{}{command}{print\_facts}\hypertarget{command.print-facts}{\hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
     \indexdef{}{command}{print\_binds}\hypertarget{command.print-binds}{\hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
@@ -45,11 +46,15 @@
     'print\_theory' ( '!'?)
     ;
 
-    'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *)
+    'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (thmcriterion *)
     ;
-    criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
+    thmcriterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
       'solves' | 'simp' ':' term | term)
     ;
+    'find\_consts' (constcriterion +)
+    ;
+    constcriterion: ('-'?) ('name' ':' nameref | 'strict' ':' type | type)
+    ;
     'thm\_deps' thmrefs
     ;
   \end{rail}
@@ -97,7 +102,14 @@
   number of printed facts may be given; the default is 40.  By
   default, duplicates are removed from the search result. Use
   \isa{with{\isacharunderscore}dups} to display duplicates.
-  
+
+  \item \hyperlink{command.find-consts}{\mbox{\isa{\isacommand{find{\isacharunderscore}consts}}}}~\isa{criteria} prints all constants
+  whose type meets all of the given criteria. The criterion \isa{{\isachardoublequote}strict{\isacharcolon}\ ty{\isachardoublequote}} is met by any type that matches the type pattern
+  \isa{ty}.  Patterns may contain both the dummy type ``\isa{{\isacharunderscore}}''
+  and sort constraints. The criterion \isa{ty} is similar, but it
+  also matches against subtypes. The criterion \isa{{\isachardoublequote}name{\isacharcolon}\ p{\isachardoublequote}} and
+  the prefix ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' function as described for \hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}.
+
   \item \hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}
   visualizes dependencies of facts, using Isabelle's graph browser
   tool (see also \cite{isabelle-sys}).