src/ZF/AC/ROOT.ML
author wenzelm
Mon, 05 Nov 2007 20:50:44 +0100
changeset 25291 870455627720
parent 23912 039ae566a4a2
child 32960 69916a850301
permissions -rw-r--r--
misc cleanup of init functions; renamed init_cmd to context; simplified LocalTheory.reinit;

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

Proofs of AC-equivalences, due to Krzysztof Grabczewski.
*)

use_thys ["WO6_WO1", "WO1_WO7", "AC7_AC9", "WO1_AC", "AC15_WO6",
  "WO2_AC16", "AC16_WO4", "AC17_AC1", "AC18_AC19", "DC"];