| changeset 45800 | e832acb88f43 |
| parent 45577 | 33b964e117bd |
| child 45815 | 2b7eb46e70f9 |
--- a/src/HOL/Quotient_Examples/ROOT.ML Fri Dec 09 14:22:05 2011 +0100 +++ b/src/HOL/Quotient_Examples/ROOT.ML Fri Dec 09 14:46:18 2011 +0100 @@ -5,5 +5,5 @@ *) use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Cset", - "List_Quotient_Cset", "Lift_Set", "Lift_RBT"]; + "List_Quotient_Cset", "Lift_Set", "Lift_RBT", "Lift_Fun"];