src/ZF/AC/ROOT.ML
author wenzelm
Sat, 01 Mar 2008 14:10:15 +0100
changeset 26189 9808cca5c54d
parent 23912 039ae566a4a2
child 32960 69916a850301
permissions -rw-r--r--
misc cleanup of embedded ML code; use more antiquotations; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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"];