# HG changeset patch # User berghofe # Date 1295741022 -3600 # Node ID 237328506a4202f2c341a7308b5fb01b9c64a1cd # Parent f5619d83d0e308d9305f58514b98f4111592b5a8 Documented unused_thms diff -r f5619d83d0e3 -r 237328506a42 doc-src/IsarRef/Thy/Misc.thy --- a/doc-src/IsarRef/Thy/Misc.thy Fri Jan 21 22:04:12 2011 +0100 +++ b/doc-src/IsarRef/Thy/Misc.thy Sun Jan 23 01:03:42 2011 +0100 @@ -16,6 +16,7 @@ @{command_def "find_theorems"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{command_def "find_consts"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{command_def "thm_deps"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "unused_thms"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \"} \\ \end{matharray} @@ -35,6 +36,8 @@ ; 'thm_deps' thmrefs ; + 'unused_thms' (('name'+) '-' ('name'*))? + ; \end{rail} These commands print certain parts of the theory and proof context. @@ -93,6 +96,13 @@ \item @{command "thm_deps"}~@{text "a\<^sub>1 \ a\<^sub>n"} visualizes dependencies of facts, using Isabelle's graph browser tool (see also \cite{isabelle-sys}). + + \item @{command "unused_thms"}~@{text "A\<^isub>1 \ A\<^isub>m - B\<^isub>1 \ B\<^isub>n"} + displays all unused theorems in theories @{text "B\<^isub>1 \ B\<^isub>n"} + or their parents, but not in @{text "A\<^isub>1 \ A\<^isub>m"} or their parents. + 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. \item @{command "print_facts"} prints all local facts of the current context, both named and unnamed ones. diff -r f5619d83d0e3 -r 237328506a42 doc-src/IsarRef/Thy/document/Misc.tex --- a/doc-src/IsarRef/Thy/document/Misc.tex Fri Jan 21 22:04:12 2011 +0100 +++ b/doc-src/IsarRef/Thy/document/Misc.tex Sun Jan 23 01:03:42 2011 +0100 @@ -36,6 +36,7 @@ \indexdef{}{command}{find\_theorems}\hypertarget{command.find-theorems}{\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}theorems}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\ \indexdef{}{command}{find\_consts}\hypertarget{command.find-consts}{\hyperlink{command.find-consts}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}consts}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\ \indexdef{}{command}{thm\_deps}\hypertarget{command.thm-deps}{\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isaliteral{5F}{\isacharunderscore}}deps}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\ + \indexdef{}{command}{unused\_thms}\hypertarget{command.unused-thms}{\hyperlink{command.unused-thms}{\mbox{\isa{\isacommand{unused{\isaliteral{5F}{\isacharunderscore}}thms}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\ \indexdef{}{command}{print\_facts}\hypertarget{command.print-facts}{\hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}facts}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\ \indexdef{}{command}{print\_binds}\hypertarget{command.print-binds}{\hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}binds}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\ \end{matharray} @@ -55,6 +56,8 @@ ; 'thm_deps' thmrefs ; + 'unused_thms' (('name'+) '-' ('name'*))? + ; \end{rail} These commands print certain parts of the theory and proof context. @@ -111,6 +114,13 @@ \item \hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isaliteral{5F}{\isacharunderscore}}deps}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} visualizes dependencies of facts, using Isabelle's graph browser tool (see also \cite{isabelle-sys}). + + \item \hyperlink{command.unused-thms}{\mbox{\isa{\isacommand{unused{\isaliteral{5F}{\isacharunderscore}}thms}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub m\ {\isaliteral{2D}{\isacharminus}}\ B\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ B\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} + displays all unused theorems in theories \isa{{\isaliteral{22}{\isachardoublequote}}B\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ B\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} + or their parents, but not in \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub m{\isaliteral{22}{\isachardoublequote}}} or their parents. + If \isa{n} is \isa{{\isadigit{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. \item \hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}facts}}}} prints all local facts of the current context, both named and unnamed ones.