equal
deleted
inserted
replaced
1 Highest Priority |
1 Highest Priority |
2 ================ |
2 ================ |
3 |
3 |
4 Higher Priority |
4 Higher Priority |
5 =============== |
5 =============== |
|
6 |
|
7 - Ask Markus how the files Quot* should be named. |
|
8 (There is a HOL/Library/Quotient.thy --- seems to be an example. *) |
|
9 |
|
10 - Is Bexeq the right name? |
|
11 |
6 |
12 |
7 - If the constant definition gives the wrong definition |
13 - If the constant definition gives the wrong definition |
8 term, one gets a cryptic message about absrep_fun |
14 term, one gets a cryptic message about absrep_fun |
9 |
15 |
10 - Handle theorems that include Ball/Bex. For this, would |
16 - Handle theorems that include Ball/Bex. For this, would |