isabelle: src/ZF/AC/ROOT.ML@bbb5e6904d78 (annotated)

23912 039ae566a4a2 simultaneous use_thys; wenzelm parents: 12776 diff changeset	1	(* Title: ZF/AC/ROOT.ML
992 4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1351 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
992 4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	4	Copyright 1995 University of Cambridge
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	5
23912 039ae566a4a2 simultaneous use_thys; wenzelm parents: 12776 diff changeset	6	Proofs of AC-equivalences, due to Krzysztof Grabczewski.
992 4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	7	*)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	8
23912 039ae566a4a2 simultaneous use_thys; wenzelm parents: 12776 diff changeset	9	use_thys ["WO6_WO1", "WO1_WO7", "AC7_AC9", "WO1_AC", "AC15_WO6",
039ae566a4a2 simultaneous use_thys; wenzelm parents: 12776 diff changeset	10	"WO2_AC16", "AC16_WO4", "AC17_AC1", "AC18_AC19", "DC"];