equal
deleted
inserted
replaced
14 @{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
14 @{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
15 @{command_def "print_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
15 @{command_def "print_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
16 @{command_def "find_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
16 @{command_def "find_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
17 @{command_def "find_consts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
17 @{command_def "find_consts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
18 @{command_def "thm_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
18 @{command_def "thm_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
19 @{command_def "unused_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
19 @{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
20 @{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
20 @{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
21 @{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
21 \end{matharray} |
22 \end{matharray} |
22 |
23 |
23 \begin{rail} |
24 \begin{rail} |
32 'find_consts' (constcriterion *) |
33 'find_consts' (constcriterion *) |
33 ; |
34 ; |
34 constcriterion: ('-'?) ('name' ':' nameref | 'strict' ':' type | type) |
35 constcriterion: ('-'?) ('name' ':' nameref | 'strict' ':' type | type) |
35 ; |
36 ; |
36 'thm_deps' thmrefs |
37 'thm_deps' thmrefs |
|
38 ; |
|
39 'unused_thms' (('name'+) '-' ('name'*))? |
37 ; |
40 ; |
38 \end{rail} |
41 \end{rail} |
39 |
42 |
40 These commands print certain parts of the theory and proof context. |
43 These commands print certain parts of the theory and proof context. |
41 Note that there are some further ones available, such as for the set |
44 Note that there are some further ones available, such as for the set |
91 "find_theorems"}. |
94 "find_theorems"}. |
92 |
95 |
93 \item @{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} |
96 \item @{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} |
94 visualizes dependencies of facts, using Isabelle's graph browser |
97 visualizes dependencies of facts, using Isabelle's graph browser |
95 tool (see also \cite{isabelle-sys}). |
98 tool (see also \cite{isabelle-sys}). |
|
99 |
|
100 \item @{command "unused_thms"}~@{text "A\<^isub>1 \<dots> A\<^isub>m - B\<^isub>1 \<dots> B\<^isub>n"} |
|
101 displays all unused theorems in theories @{text "B\<^isub>1 \<dots> B\<^isub>n"} |
|
102 or their parents, but not in @{text "A\<^isub>1 \<dots> A\<^isub>m"} or their parents. |
|
103 If @{text n} is @{text 0}, the end of the range of theories |
|
104 defaults to the current theory. If no range is specified, |
|
105 only the unused theorems in the current theory are displayed. |
96 |
106 |
97 \item @{command "print_facts"} prints all local facts of the |
107 \item @{command "print_facts"} prints all local facts of the |
98 current context, both named and unnamed ones. |
108 current context, both named and unnamed ones. |
99 |
109 |
100 \item @{command "print_binds"} prints all term abbreviations |
110 \item @{command "print_binds"} prints all term abbreviations |