Theory Lists_are_Infinite

(*
Author:  Christian Sternagel <c.sternagel@gmail.com>
Author:  René Thiemann <rene.thiemann@uibk.ac.at>
License: LGPL
*)
subsection ‹Make lists instances of the infinite-class.›

theory Lists_are_Infinite
  imports Fresh_Identifiers.Fresh
begin

instance list :: (type) infinite
  by (intro_classes, rule infinite_UNIV_listI)

end