src/HOL/Quotient_Examples/ROOT.ML
changeset 36524 3909002beca5
parent 36280 c4f5823f282d
child 43766 9545bb3cefac
equal deleted inserted replaced
36523:a294e4ebe0a3 36524:3909002beca5
     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 ["FSet", "LarryInt", "LarryDatatype"];
     7 use_thys ["FSet", "Quotient_Int", "Quotient_Message"];
     8 
     8