src/ZF/AC/ROOT.ML

removed foo_build_completed -- now handled by session management (via usedir);

(*  Title:      ZF/AC/ROOT
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1995  University of Cambridge

Executes the proofs of the AC-equivalences, due to Krzysztof Grabczewski
*)

writeln"Root file for ZF/AC";
set proof_timing;

time_use_thy "AC_Equiv";

time_use     "WO1_WO6.ML";
time_use_thy "WO6_WO1";
time_use_thy "WO1_WO7";
time_use     "WO1_WO8.ML";

time_use     "AC0_AC1.ML";
time_use     "AC2_AC6.ML";
time_use     "AC7_AC9.ML";

time_use_thy "WO1_AC";
time_use_thy "AC1_WO2";

time_use     "AC10_AC15.ML";
time_use_thy "AC15_WO6";

time_use_thy "WO2_AC16";
time_use_thy "AC16_WO4";

time_use     "AC1_AC17.ML";
time_use_thy "AC17_AC1";

time_use_thy "AC18_AC19";

time_use_thy "DC";

writeln"END: Root file for ZF/AC";