Семинар 6. Объявление типов в Isabelle/HOL. Рекурсивные функции. Индукция