| changeset 1463 | 1909be313353 |
| parent 1460 | 0fd03936dedb |
| 1462:7c59dd8e5435 | 1463:1909be313353 |
|---|---|
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") |