equal
deleted
inserted
replaced
1 Highest Priority |
1 Highest Priority |
2 ================ |
2 ================ |
3 |
3 |
4 - better lookup mechanism for quotient definition |
|
5 (see fixme in quotient_term.ML) |
|
6 |
|
7 Higher Priority |
4 Higher Priority |
8 =============== |
5 =============== |
9 |
|
10 - If the user defines twice the same quotient constant, |
|
11 for example funion, then the line |
|
12 |
|
13 val Free (lhs_str, lhs_ty) = lhs |
|
14 |
|
15 in quotient_def raises a bind exception. |
|
16 |
6 |
17 - If the constant definition gives the wrong definition |
7 - If the constant definition gives the wrong definition |
18 term, one gets a cryptic message about absrep_fun |
8 term, one gets a cryptic message about absrep_fun |
19 |
9 |
20 - Handle theorems that include Ball/Bex. For this, would |
10 - Handle theorems that include Ball/Bex. For this, would |