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