(* Title: HOL/List.thy Author: Tobias Nipkow; proofs tidied by LCP *) section ‹The datatype of finite lists› theory List imports Sledgehammer Lifting_Set begin