src/HOL/Quotient_Examples/ROOT.ML
changeset 45319 2b002c6b0f7d
parent 45267 66823a0066db
child 45536 5b0b1dc2e40f
equal deleted inserted replaced
45318:e72018e0dd75 45319:2b002c6b0f7d
     2     Author:     Cezary Kaliszyk and Christian Urban
     2     Author:     Cezary Kaliszyk and Christian Urban
     3 
     3 
     4 Testing the quotient package.
     4 Testing the quotient package.
     5 *)
     5 *)
     6 
     6 
     7 use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Set", "List_Quotient_Set"];
     7 use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Cset", "List_Quotient_Cset"];
     8 
     8