src/ZF/List_ZF.thy
changeset 35068 544867142ea4
parent 32960 69916a850301
child 35112 ff6f60e6ab85
equal deleted inserted replaced
35067:af4c18c30593 35068:544867142ea4
    17 syntax
    17 syntax
    18  "[]"        :: i                                       ("[]")
    18  "[]"        :: i                                       ("[]")
    19  "@List"     :: "is => i"                                 ("[(_)]")
    19  "@List"     :: "is => i"                                 ("[(_)]")
    20 
    20 
    21 translations
    21 translations
    22   "[x, xs]"     == "Cons(x, [xs])"
    22   "[x, xs]"     == "CONST Cons(x, [xs])"
    23   "[x]"         == "Cons(x, [])"
    23   "[x]"         == "CONST Cons(x, [])"
    24   "[]"          == "Nil"
    24   "[]"          == "CONST Nil"
    25 
    25 
    26 
    26 
    27 consts
    27 consts
    28   length :: "i=>i"
    28   length :: "i=>i"
    29   hd     :: "i=>i"
    29   hd     :: "i=>i"