src/HOL/Quotient_Examples/ROOT.ML
changeset 35222 4f1fba00f66d
child 36280 c4f5823f282d
equal deleted inserted replaced
35221:5cb63cb4213f 35222:4f1fba00f66d
       
     1 (*  Title:      HOL/Quotient_Examples/ROOT.ML
       
     2     Author:     Cezary Kaliszyk and Christian Urban
       
     3 
       
     4 Testing the quotient package.
       
     5 *)
       
     6 
       
     7 use_thys ["LarryInt", "LarryDatatype"];
       
     8