| changeset 47232 | e2f0176149d0 |
| parent 45815 | 2b7eb46e70f9 |
| child 47308 | 9caab698dbe4 |
--- a/src/HOL/Quotient_Examples/ROOT.ML Fri Mar 30 17:25:34 2012 +0200 +++ b/src/HOL/Quotient_Examples/ROOT.ML Fri Mar 30 18:56:02 2012 +0200 @@ -4,6 +4,6 @@ Testing the quotient package. *) -use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Cset", - "List_Quotient_Cset", "Lift_Set", "Lift_RBT", "Lift_Fun", "Quotient_Rat"]; +use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", + "Lift_Set", "Lift_RBT", "Lift_Fun", "Quotient_Rat"];