| changeset 1460 | 0fd03936dedb |
| parent 1260 | 9df6144e281b |
| 1459:d6d22254aeb7 | 1460:0fd03936dedb |
|---|---|
1 (* Title: Quotient.thy |
1 (* Title: Quotient.thy |
2 Author: Cezary Kaliszyk and Christian Urban |
2 Author: Cezary Kaliszyk and Christian Urban |
3 *) |
3 *) |
4 |
4 |
5 theory Quotient |
5 theory Quotient |
6 imports Plain ATP_Linkup |
6 imports Plain ATP_Linkup |
7 uses |
7 uses |
8 ("quotient_info.ML") |
8 ("quotient_info.ML") |
9 ("quotient_typ.ML") |
9 ("quotient_typ.ML") |
10 ("quotient_def.ML") |
10 ("quotient_def.ML") |
11 ("quotient_term.ML") |
11 ("quotient_term.ML") |