author | wenzelm |
Fri, 13 Aug 2010 21:30:10 +0200 | |
changeset 38371 | 5b615a4a3a68 |
parent 32960 | 69916a850301 |
permissions | -rw-r--r-- |
23912 | 1 |
(* Title: ZF/AC/ROOT.ML |
1461 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
992 | 3 |
Copyright 1995 University of Cambridge |
4 |
||
23912 | 5 |
Proofs of AC-equivalences, due to Krzysztof Grabczewski. |
992 | 6 |
*) |
7 |
||
23912 | 8 |
use_thys ["WO6_WO1", "WO1_WO7", "AC7_AC9", "WO1_AC", "AC15_WO6", |
9 |
"WO2_AC16", "AC16_WO4", "AC17_AC1", "AC18_AC19", "DC"]; |