equal
deleted
inserted
replaced
1 (* Title: HOL/Quotient_Examples/FSet.thy |
1 (* Title: HOL/Quotient_Examples/FSet.thy |
2 Author: Cezary Kaliszyk, TU Munich |
2 Author: Cezary Kaliszyk, TU Munich |
3 Author: Christian Urban, TU Munich |
3 Author: Christian Urban, TU Munich |
4 |
4 |
5 Type of finite sets. |
5 Type of finite sets. |
6 *) |
6 *) |
7 |
7 |
8 theory FSet |
8 theory FSet |
9 imports "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/More_List" |
9 imports "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/More_List" |
10 begin |
10 begin |