src/HOL/List.thy
changeset 18702 7dc7dcd63224
parent 18622 4524643feecc
child 18704 2c86ced392a8
     1.1 --- a/src/HOL/List.thy	Tue Jan 17 10:26:50 2006 +0100
     1.2 +++ b/src/HOL/List.thy	Tue Jan 17 16:36:57 2006 +0100
     1.3 @@ -2684,6 +2684,23 @@
     1.4  
     1.5  consts_code "Cons" ("(_ ::/ _)")
     1.6  
     1.7 +code_alias
     1.8 +  "List.op @" "List.append"
     1.9 +  "List.op mem" "List.member"
    1.10 +
    1.11 +code_syntax_tyco
    1.12 +  list
    1.13 +    ml ("_ list")
    1.14 +    haskell (atom "[_]")
    1.15 +
    1.16 +code_syntax_const
    1.17 +  Nil
    1.18 +    ml (atom "[]")
    1.19 +    haskell (atom "[]")
    1.20 +  Cons
    1.21 +    ml (infixr 7 "::" )
    1.22 +    haskell (infixr 5 ":")
    1.23 +
    1.24  setup list_codegen_setup
    1.25  
    1.26  setup "[CodegenPackage.rename_inconsistent]"