src/HOL/List.thy
changeset 24219 e558fe311376
parent 24166 7b28dc69bdbb
child 24286 7619080e49f0
equal deleted inserted replaced
24218:fbf1646b267c 24219:e558fe311376
  2813   (SML "[]")
  2813   (SML "[]")
  2814   (OCaml "[]")
  2814   (OCaml "[]")
  2815   (Haskell "[]")
  2815   (Haskell "[]")
  2816 
  2816 
  2817 setup {*
  2817 setup {*
  2818   fold (fn target => CodegenSerializer.add_pretty_list target
  2818   fold (fn target => CodeTarget.add_pretty_list target
  2819     @{const_name Nil} @{const_name Cons}
  2819     @{const_name Nil} @{const_name Cons}
  2820   ) ["SML", "OCaml", "Haskell"]
  2820   ) ["SML", "OCaml", "Haskell"]
  2821 *}
  2821 *}
  2822 
  2822 
  2823 code_instance list :: eq
  2823 code_instance list :: eq