equal
deleted
inserted
replaced
97 the prefix ``@{text "-"}'' function as described for @{command |
97 the prefix ``@{text "-"}'' function as described for @{command |
98 "find_theorems"}. |
98 "find_theorems"}. |
99 |
99 |
100 \item @{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} |
100 \item @{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} |
101 visualizes dependencies of facts, using Isabelle's graph browser |
101 visualizes dependencies of facts, using Isabelle's graph browser |
102 tool (see also \cite{isabelle-sys}). |
102 tool (see also @{cite "isabelle-sys"}). |
103 |
103 |
104 \item @{command "unused_thms"}~@{text "A\<^sub>1 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n"} |
104 \item @{command "unused_thms"}~@{text "A\<^sub>1 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n"} |
105 displays all theorems that are proved in theories @{text "B\<^sub>1 \<dots> B\<^sub>n"} |
105 displays all theorems that are proved in theories @{text "B\<^sub>1 \<dots> B\<^sub>n"} |
106 or their parents but not in @{text "A\<^sub>1 \<dots> A\<^sub>m"} or their parents and |
106 or their parents but not in @{text "A\<^sub>1 \<dots> A\<^sub>m"} or their parents and |
107 that are never used. |
107 that are never used. |