| changeset 13761 | 52d1b293da7f |
| parent 13759 | aa7360806a19 |
| 13760:2188f247605c | 13761:52d1b293da7f |
|---|---|
2 add the SET protocol proofs to HOL/Auth |
2 add the SET protocol proofs to HOL/Auth |
3 add Quadratic Reciprocity |
3 add Quadratic Reciprocity |
4 complete the new formalization of Group theory |
4 complete the new formalization of Group theory |
5 |
5 |
6 add Presburger arithmetic (if possible until March) |
6 add Presburger arithmetic (if possible until March) |
7 stop eta-contraction for binders |