--- a/src/Doc/Isar_Ref/Misc.thy Mon Jul 06 20:07:41 2015 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,119 +0,0 @@
-theory Misc
-imports Base Main
-begin
-
-chapter \<open>Other commands\<close>
-
-section \<open>Inspecting the context\<close>
-
-text \<open>
- \begin{matharray}{rcl}
- @{command_def "print_theory"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{command_def "print_methods"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{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 "unused_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{command_def "print_term_bindings"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- \end{matharray}
-
- @{rail \<open>
- (@@{command print_theory} |
- @@{command print_methods} |
- @@{command print_attributes} |
- @@{command print_theorems} |
- @@{command print_facts}) ('!'?)
- ;
- @@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \<newline> (thm_criterion*)
- ;
- thm_criterion: ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' |
- 'solves' | 'simp' ':' @{syntax term} | @{syntax term})
- ;
- @@{command find_consts} (const_criterion*)
- ;
- const_criterion: ('-'?)
- ('name' ':' @{syntax nameref} | 'strict' ':' @{syntax type} | @{syntax type})
- ;
- @@{command thm_deps} @{syntax thmrefs}
- ;
- @@{command unused_thms} ((@{syntax name} +) '-' (@{syntax name} * ))?
- \<close>}
-
- These commands print certain parts of the theory and proof context.
- Note that there are some further ones available, such as for the set
- of rules declared for simplifications.
-
- \begin{description}
-
- \item @{command "print_theory"} prints the main logical content of the
- background theory; the ``@{text "!"}'' option indicates extra verbosity.
-
- \item @{command "print_methods"} prints all proof methods available in the
- current theory context; the ``@{text "!"}'' option indicates extra
- verbosity.
-
- \item @{command "print_attributes"} prints all attributes available in the
- current theory context; the ``@{text "!"}'' option indicates extra
- verbosity.
-
- \item @{command "print_theorems"} prints theorems of the background theory
- resulting from the last command; the ``@{text "!"}'' option indicates
- extra verbosity.
-
- \item @{command "print_facts"} prints all local facts of the current
- context, both named and unnamed ones; the ``@{text "!"}'' option indicates
- extra verbosity.
-
- \item @{command "print_term_bindings"} prints all term bindings that
- are present in the context.
-
- \item @{command "find_theorems"}~@{text criteria} retrieves facts
- from the theory or proof context matching all of given search
- criteria. The criterion @{text "name: p"} selects all theorems
- whose fully qualified name matches pattern @{text p}, which may
- 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 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
- theorems that contain the pattern @{text t} -- as usual, patterns
- may contain occurrences of the dummy ``@{text _}'', schematic
- variables, and type constraints.
-
- Criteria can be preceded by ``@{text "-"}'' to select theorems that
- do \emph{not} match. Note that giving the empty list of criteria
- yields \emph{all} currently known facts. An optional limit for the
- 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-system"}).
-
- \item @{command "unused_thms"}~@{text "A\<^sub>1 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n"}
- displays all theorems that are proved in theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}
- or their parents but not in @{text "A\<^sub>1 \<dots> A\<^sub>m"} or their parents and
- that are never used.
- If @{text n} is @{text 0}, the end of the range of theories
- defaults to the current theory. If no range is specified,
- only the unused theorems in the current theory are displayed.
-
- \end{description}
-\<close>
-
-end
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Mon Jul 06 20:07:41 2015 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Mon Jul 06 20:13:51 2015 +0200
@@ -411,7 +411,7 @@
There are three forms of theorem references:
\begin{enumerate}
-
+
\item named facts @{text "a"},
\item selections from named facts @{text "a(i)"} or @{text "a(j - k)"},
@@ -456,4 +456,117 @@
\<close>}
\<close>
+
+section \<open>Diagnostic commands\<close>
+
+text \<open>
+ \begin{matharray}{rcl}
+ @{command_def "print_theory"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "print_methods"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{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 "unused_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "print_term_bindings"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ \end{matharray}
+
+ @{rail \<open>
+ (@@{command print_theory} |
+ @@{command print_methods} |
+ @@{command print_attributes} |
+ @@{command print_theorems} |
+ @@{command print_facts}) ('!'?)
+ ;
+ @@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \<newline> (thm_criterion*)
+ ;
+ thm_criterion: ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' |
+ 'solves' | 'simp' ':' @{syntax term} | @{syntax term})
+ ;
+ @@{command find_consts} (const_criterion*)
+ ;
+ const_criterion: ('-'?)
+ ('name' ':' @{syntax nameref} | 'strict' ':' @{syntax type} | @{syntax type})
+ ;
+ @@{command thm_deps} @{syntax thmrefs}
+ ;
+ @@{command unused_thms} ((@{syntax name} +) '-' (@{syntax name} * ))?
+ \<close>}
+
+ These commands print certain parts of the theory and proof context.
+ Note that there are some further ones available, such as for the set
+ of rules declared for simplifications.
+
+ \begin{description}
+
+ \item @{command "print_theory"} prints the main logical content of the
+ background theory; the ``@{text "!"}'' option indicates extra verbosity.
+
+ \item @{command "print_methods"} prints all proof methods available in the
+ current theory context; the ``@{text "!"}'' option indicates extra
+ verbosity.
+
+ \item @{command "print_attributes"} prints all attributes available in the
+ current theory context; the ``@{text "!"}'' option indicates extra
+ verbosity.
+
+ \item @{command "print_theorems"} prints theorems of the background theory
+ resulting from the last command; the ``@{text "!"}'' option indicates
+ extra verbosity.
+
+ \item @{command "print_facts"} prints all local facts of the current
+ context, both named and unnamed ones; the ``@{text "!"}'' option indicates
+ extra verbosity.
+
+ \item @{command "print_term_bindings"} prints all term bindings that
+ are present in the context.
+
+ \item @{command "find_theorems"}~@{text criteria} retrieves facts
+ from the theory or proof context matching all of given search
+ criteria. The criterion @{text "name: p"} selects all theorems
+ whose fully qualified name matches pattern @{text p}, which may
+ 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 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
+ theorems that contain the pattern @{text t} -- as usual, patterns
+ may contain occurrences of the dummy ``@{text _}'', schematic
+ variables, and type constraints.
+
+ Criteria can be preceded by ``@{text "-"}'' to select theorems that
+ do \emph{not} match. Note that giving the empty list of criteria
+ yields \emph{all} currently known facts. An optional limit for the
+ 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-system"}).
+
+ \item @{command "unused_thms"}~@{text "A\<^sub>1 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n"}
+ displays all theorems that are proved in theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}
+ or their parents but not in @{text "A\<^sub>1 \<dots> A\<^sub>m"} or their parents and
+ that are never used.
+ If @{text n} is @{text 0}, the end of the range of theories
+ defaults to the current theory. If no range is specified,
+ only the unused theorems in the current theory are displayed.
+
+ \end{description}
+\<close>
+
end
--- a/src/Doc/Isar_Ref/document/root.tex Mon Jul 06 20:07:41 2015 +0200
+++ b/src/Doc/Isar_Ref/document/root.tex Mon Jul 06 20:13:51 2015 +0200
@@ -76,7 +76,6 @@
\input{Proof.tex}
\input{Proof_Script.tex}
\input{Inner_Syntax.tex}
-\input{Misc.tex}
\input{Generic.tex}
\part{Isabelle/HOL}\label{part:hol}
\input{HOL_Specific.tex}
--- a/src/Doc/ROOT Mon Jul 06 20:07:41 2015 +0200
+++ b/src/Doc/ROOT Mon Jul 06 20:13:51 2015 +0200
@@ -166,7 +166,6 @@
Proof
Proof_Script
Inner_Syntax
- Misc
Generic
HOL_Specific
Quick_Reference