author | krauss |
Wed, 13 Jul 2011 15:50:45 +0200 | |
changeset 43800 | 9959c8732edf |
parent 43766 | 9545bb3cefac |
child 45267 | 66823a0066db |
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 |
|
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
43766
diff
changeset
|
7 |
use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Cset", "List_Cset"]; |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
8 |