31 space take precedence. INCOMPATIBILITY in rare situations, may try to |
31 space take precedence. INCOMPATIBILITY in rare situations, may try to |
32 swap theory imports. |
32 swap theory imports. |
33 |
33 |
34 |
34 |
35 *** Pure *** |
35 *** Pure *** |
|
36 |
|
37 * Unused theorems can be found using the new command 'unused_thms'. |
|
38 There are three ways of invoking it: |
|
39 |
|
40 (1) unused_thms |
|
41 Only finds unused theorems in the current theory. |
|
42 |
|
43 (2) unused_thms thy_1 ... thy_n - |
|
44 Finds unused theorems in the current theory and all of its ancestors, |
|
45 excluding the theories thy_1 ... thy_n and all of their ancestors. |
|
46 |
|
47 (3) unused_thms thy_1 ... thy_n - thy'_1 ... thy'_m |
|
48 Finds unused theorems in the theories thy'_1 ... thy'_m and all of |
|
49 their ancestors, excluding the theories thy_1 ... thy_n and all of |
|
50 their ancestors. |
|
51 |
|
52 In order to increase the readability of the list produced by unused_thms, |
|
53 theorems that have been created by a particular instance of a theory |
|
54 command such as inductive or fun(ction) are considered to belong to the |
|
55 same "group", meaning that if at least one theorem in this group is used, |
|
56 the other theorems in the same group are no longer reported as unused. |
|
57 Moreover, if all theorems in the group are unused, only one theorem in |
|
58 the group is displayed. |
|
59 Note that proof objects have to be switched on in order for unused_thms |
|
60 to work properly (i.e. !proofs must be >= 1, which is usually the case |
|
61 when using ProofGeneral with the default settings). |
36 |
62 |
37 * Authentic naming of facts disallows ad-hoc overwriting of previous |
63 * Authentic naming of facts disallows ad-hoc overwriting of previous |
38 theorems within the same name space. INCOMPATIBILITY, need to remove |
64 theorems within the same name space. INCOMPATIBILITY, need to remove |
39 duplicate fact bindings, or even accidental fact duplications. Note |
65 duplicate fact bindings, or even accidental fact duplications. Note |
40 that tools may maintain dynamically scoped facts systematically, using |
66 that tools may maintain dynamically scoped facts systematically, using |