src/ZF/AC/ROOT.ML

legacy_infer_term/prop -- including intern_term;

(*  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
*)

time_use_thy "WO6_WO1";
time_use_thy "WO1_WO7";

time_use_thy "AC7_AC9";

time_use_thy "WO1_AC";

time_use_thy "AC15_WO6";

time_use_thy "WO2_AC16";
time_use_thy "AC16_WO4";

time_use_thy "AC17_AC1";

time_use_thy "AC18_AC19";

time_use_thy "DC";