changeset 19890 | 1aad48bcc674 |
parent 19817 | bb16bf9ae3fd |
child 20044 | 92cc2f4c7335 |
--- a/src/HOL/List.thy Wed Jun 14 12:14:13 2006 +0200 +++ b/src/HOL/List.thy Wed Jun 14 12:14:42 2006 +0200 @@ -2737,17 +2737,17 @@ "List.op @" "List.append" "List.op mem" "List.mem" -code_syntax_tyco +code_typapp list ml ("_ list") haskell (target_atom "[_]") -code_syntax_const +code_constapp Nil ml (target_atom "[]") haskell (target_atom "[]") -code_syntax_tyco +code_typapp char ml (target_atom "char") haskell (target_atom "Char")