equal
deleted
inserted
replaced
1 (* Title: HOL/Finite_Set.thy |
1 (* Title: HOL/Finite_Set.thy |
2 Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel |
2 Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel |
3 with contributions by Jeremy Avigad and Andrei Popescu |
3 with contributions by Jeremy Avigad and Andrei Popescu |
4 *) |
4 *) |
5 |
5 |
6 header {* Finite sets *} |
6 section {* Finite sets *} |
7 |
7 |
8 theory Finite_Set |
8 theory Finite_Set |
9 imports Product_Type Sum_Type Nat |
9 imports Product_Type Sum_Type Nat |
10 begin |
10 begin |
11 |
11 |