| changeset 43800 | 9959c8732edf |
| parent 43766 | 9545bb3cefac |
| child 45267 | 66823a0066db |
--- a/src/HOL/Quotient_Examples/ROOT.ML Wed Jul 13 04:00:32 2011 +0900 +++ b/src/HOL/Quotient_Examples/ROOT.ML Wed Jul 13 15:50:45 2011 +0200 @@ -4,5 +4,5 @@ Testing the quotient package. *) -use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message"]; +use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Cset", "List_Cset"];