13759
|
1 |
finish converting ZF to new-style theories
|
|
2 |
add the SET protocol proofs to HOL/Auth
|
|
3 |
add Quadratic Reciprocity
|
|
4 |
complete the new formalization of Group theory
|
|
5 |
|
|
6 |
add Presburger arithmetic (if possible until March)
|
13761
|
7 |
stop eta-contraction for binders
|