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

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