(* Title: ZF/AC/ROOT ID: $Id: ROOT.ML,v 1.15 2002/01/16 16:52:15 paulson Exp $ 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";