src/ZF/AC/ROOT.ML
author wenzelm
Tue May 30 16:08:38 2000 +0200 (2000-05-30)
changeset 9000 c20d58286a51
parent 6349 f7750d816c21
child 11380 e76366922751
permissions -rw-r--r--
cleaned up;
     1 (*  Title:      ZF/AC/ROOT
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1995  University of Cambridge
     5 
     6 Executes the proofs of the AC-equivalences, due to Krzysztof Grabczewski
     7 *)
     8 
     9 time_use_thy "AC_Equiv";
    10 
    11 time_use     "WO1_WO6.ML";
    12 time_use_thy "WO6_WO1";
    13 time_use_thy "WO1_WO7";
    14 time_use     "WO1_WO8.ML";
    15 
    16 time_use     "AC0_AC1.ML";
    17 time_use     "AC2_AC6.ML";
    18 time_use     "AC7_AC9.ML";
    19 
    20 time_use_thy "WO1_AC";
    21 time_use_thy "AC1_WO2";
    22 
    23 time_use     "AC10_AC15.ML";
    24 time_use_thy "AC15_WO6";
    25 
    26 time_use_thy "WO2_AC16";
    27 time_use_thy "AC16_WO4";
    28 
    29 time_use     "AC1_AC17.ML";
    30 time_use_thy "AC17_AC1";
    31 
    32 time_use_thy "AC18_AC19";
    33 
    34 time_use_thy "DC";