src/ZF/AC/AC_Equiv.thy
changeset 1401 0c439768f45c
parent 1203 a39bec971684
child 1478 2b8c2a7547ab
     1.1 --- a/src/ZF/AC/AC_Equiv.thy	Fri Dec 08 19:48:15 1995 +0100
     1.2 +++ b/src/ZF/AC/AC_Equiv.thy	Sat Dec 09 13:36:11 1995 +0100
     1.3 @@ -17,19 +17,19 @@
     1.4  consts
     1.5    
     1.6  (* Well Ordering Theorems *)
     1.7 -  WO1, WO2, WO3, WO5, WO6, WO7, WO8 :: "o"
     1.8 -  WO4                               :: "i => o"
     1.9 +  WO1, WO2, WO3, WO5, WO6, WO7, WO8 :: o
    1.10 +  WO4                               :: i => o
    1.11  
    1.12  (* Axioms of Choice *)  
    1.13    AC0, AC1, AC2, AC3, AC4, AC5, AC6, AC7, AC8, AC9,
    1.14 -  AC11, AC12, AC14, AC15, AC17, AC19 :: "o"
    1.15 -  AC10, AC13              :: "i => o"
    1.16 -  AC16                    :: "[i, i] => o"
    1.17 -  AC18                    :: "prop"       ("AC18")
    1.18 +  AC11, AC12, AC14, AC15, AC17, AC19 :: o
    1.19 +  AC10, AC13              :: i => o
    1.20 +  AC16                    :: [i, i] => o
    1.21 +  AC18                    :: prop       ("AC18")
    1.22  
    1.23  (* Auxiliary definitions used in definitions *)
    1.24 -  pairwise_disjoint       :: "i => o"
    1.25 -  sets_of_size_between    :: "[i, i, i] => o"
    1.26 +  pairwise_disjoint       :: i => o
    1.27 +  sets_of_size_between    :: [i, i, i] => o
    1.28  
    1.29  defs
    1.30