src/HOL/Quotient_Examples/ROOT.ML
author wenzelm
Sun, 20 May 2012 11:34:33 +0200
changeset 47884 21c42b095c84
parent 47660 7a5c681c0265
child 48625 77c416ef06fa
permissions -rw-r--r--
try to avoid races again (cf. 8c37cb84065f and fd3a36e48b09);

(*  Title:      HOL/Quotient_Examples/ROOT.ML
    Author:     Cezary Kaliszyk and Christian Urban

Testing the quotient package.
*)

use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Lift_FSet",
  "Lift_Set", "Lift_RBT", "Lift_Fun", "Quotient_Rat", "Lift_DList"];