| author | wenzelm |
| Sat, 04 Oct 2008 16:05:09 +0200 | |
| changeset 28500 | 4b79e5d3d0aa |
| parent 23912 | 039ae566a4a2 |
| child 32960 | 69916a850301 |
| permissions | -rw-r--r-- |
(* 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"];