changeset 46448 | 33b964e117bd |
parent 46407 | 5b0b1dc2e40f |
child 46671 | e832acb88f43 |
1.1 --- a/src/HOL/Quotient_Examples/ROOT.ML Fri Nov 18 13:42:07 2011 +0100 1.2 +++ b/src/HOL/Quotient_Examples/ROOT.ML Fri Nov 18 13:50:01 2011 +0100 1.3 @@ -4,5 +4,6 @@ 1.4 Testing the quotient package. 1.5 *) 1.6 1.7 -use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Cset", "List_Quotient_Cset", "Lift_Set"]; 1.8 +use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Cset", 1.9 + "List_Quotient_Cset", "Lift_Set", "Lift_RBT"]; 1.10