changeset 36524 | 3909002beca5 |
parent 36465 | 15e834a03509 |
child 36639 | 6243b49498ea |
36523:a294e4ebe0a3 | 36524:3909002beca5 |
---|---|
1 (* Title: HOL/Quotient_Examples/Quotient.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 A reasoning infrastructure for the type of finite sets. |
5 A reasoning infrastructure for the type of finite sets. |
6 *) |
6 *) |