equal
deleted
inserted
replaced
1 Higher Priority |
1 Higher Priority |
2 =============== |
2 =============== |
3 |
3 |
4 - redoing Int.thy (problem at the moment with overloaded |
4 - handling constant definitions is ugly at the moment |
5 definitions....Florian) |
5 |
|
6 - if the constant definition gives the wrong definition |
|
7 term, one gets a cryptic message about get_fun |
6 |
8 |
7 - have FSet.thy to have a simple infrastructure for |
9 - have FSet.thy to have a simple infrastructure for |
8 finite sets (syntax should be \<lbrace> \<rbrace>, |
10 finite sets (syntax should be \<lbrace> \<rbrace>, |
9 look at Set.thy how syntax is been introduced) |
11 look at Set.thy how syntax is been introduced) |
10 |
12 |
13 messages for the user |
15 messages for the user |
14 |
16 |
15 - Ask Peter and Michael for challenging examples |
17 - Ask Peter and Michael for challenging examples |
16 And for examples where it is useful to lift types |
18 And for examples where it is useful to lift types |
17 over a relation being only a partial equivalence |
19 over a relation being only a partial equivalence |
18 |
|
19 |
|
20 |
20 |
21 - Handle theorems that include Ball/Bex |
21 - Handle theorems that include Ball/Bex |
22 |
22 |
23 - Test theorems with abstractions |
23 - Test theorems with abstractions |
24 |
24 |