The Isabelle/HOL theory of Lists defines lists as follows:
datatype 'a list = Nil | Cons "'a" "'a list"
This is an example of a polymorphic data type, where the type variable 'a stands for a type. For example, the type nat list is the type of lists of nat, and oot list is the type of a list of oots.
The notation x#xs is syntax sugar for Cons x xs and [] is syntax sugar for Nil. Lists can also be written in square brackets, so:
[1,2,3]
is equivalent to:
1 # 2 # 3 # []
which is equivalent to:
Cons 1 (Cons 2 (Cons 3 Nil))
Some provided functions are useful, including replicate :: nat ⇒ 'a ⇒ 'a list, which produces a list of n copies of the given value, and append :: 'a list ⇒ 'a list ⇒ 'a list which joins two lists together into one. The append function also has special notation, so a @ b is equivalent to append a b