00:15?thesis. Представление теоремы на языке Isar (повторение)
03:12Ключевое слово let. Цитирование facts по имени и по значению. Разбитие доказательства на мелкие шаги. Синтаксис для локальных лемм (повторение)
08:27Пример
13:34Теорема про квадрат разности (пример)
21:07Утверждение о существовании двух списков таких, что любой список можно представить в виде их конкатенации, причем их длины совпадают или различаются на 1 (пример)
