src/ZF/ex/Enum.thy
changeset 1401 0c439768f45c
parent 810 91c68f74f458
child 1478 2b8c2a7547ab
equal deleted inserted replaced
1400:5d909faf0e04 1401:0c439768f45c
     9 *)
     9 *)
    10 
    10 
    11 Enum = Datatype + 
    11 Enum = Datatype + 
    12 
    12 
    13 consts
    13 consts
    14   enum :: "i"
    14   enum :: i
    15 
    15 
    16 datatype
    16 datatype
    17   "enum" = C00 | C01 | C02 | C03 | C04 | C05 | C06 | C07 | C08 | C09
    17   "enum" = C00 | C01 | C02 | C03 | C04 | C05 | C06 | C07 | C08 | C09
    18          | C10 | C11 | C12 | C13 | C14 | C15 | C16 | C17 | C18 | C19
    18          | C10 | C11 | C12 | C13 | C14 | C15 | C16 | C17 | C18 | C19
    19          | C20 | C21 | C22 | C23 | C24 | C25 | C26 | C27 | C28 | C29
    19          | C20 | C21 | C22 | C23 | C24 | C25 | C26 | C27 | C28 | C29