| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Mon, 12 Dec 2011 15:32:54 +0900 | |
| changeset 45815 | 2b7eb46e70f9 |
| parent 45800 | e832acb88f43 |
| child 47232 | e2f0176149d0 |
| permissions | -rw-r--r-- |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
(* Title: HOL/Quotient_Examples/ROOT.ML |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
2 |
Author: Cezary Kaliszyk and Christian Urban |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
|
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
Testing the quotient package. |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
5 |
*) |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
|
| 45577 | 7 |
use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Cset", |
|
45815
2b7eb46e70f9
Add Quotient_Rat: an example of using the quotient package with partial equivalence relations, defining rational numbers.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
45800
diff
changeset
|
8 |
"List_Quotient_Cset", "Lift_Set", "Lift_RBT", "Lift_Fun", "Quotient_Rat"]; |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
9 |