src/HOL/ex/Seq.thy
2011-09-18 wenzelm 2011-09-18 finite sequences as useful as introductory example;