equal
deleted
inserted
replaced
12 theorem cannot be lifted) / proper diagnostic |
12 theorem cannot be lifted) / proper diagnostic |
13 messages for the user |
13 messages for the user |
14 |
14 |
15 - Handle theorems that include Ball/Bex |
15 - Handle theorems that include Ball/Bex |
16 |
16 |
17 - quotient_respects and preserves in a natural form. |
17 - user should be able to give quotient_respects and |
|
18 preserves theorems in a more natural form. |
18 |
19 |
|
20 - the test in the (_, Const _) needs to be fixed |
19 |
21 |
20 Lower Priority |
22 Lower Priority |
21 ============== |
23 ============== |
22 |
24 |
23 - accept partial equvalence relations |
25 - accept partial equvalence relations |
|
26 |
|
27 - what happens if the original theorem contains bounded |
|
28 quantifiers? can such theorems be lifted? If not, would |
|
29 it help if we introduced separate Bex and Ball constants |
|
30 for quotienting? |
24 |
31 |
25 - inductions from the datatype package have a strange |
32 - inductions from the datatype package have a strange |
26 order of quantifiers in assumptions. |
33 order of quantifiers in assumptions. |
27 |
34 |
28 - wrapper that translates an an original theorem given |
35 - wrapper that translates an an original theorem given |