Начиная с 2018 года, единственной IDE, которая поддерживается для Isabelle, является Isabelle / jEdit, которая включена в дистрибутив, который можно загрузить с веб-сайта Isabelle.Существует экспериментальный плагин VSCode, который находится в стадии активной разработки, но я бы порекомендовал использовать Isabelle / jEdit на данный момент.
Обнаруженное вами учебное пособие указано на веб-сайте как одно из «старых руководств».Он сильно устарел во многих отношениях и не должен больше использоваться.Дата публикации, вероятно, не имеет смысла, так как это дата, когда был создан PDF, а не когда текст был написан.Некоторые люди лоббировали полностью удалить это руководство с веб-сайта, и ваш опыт, похоже, подтверждает, что мы действительно должны это делать.
Один из лучших способов начать изучение Изабель, вероятно, - книга 'Семантика бетона ' (доступна бесплатная онлайн-версия).Его первая половина - в основном введение в Изабель / HOL с большим количеством упражнений.Также на веб-сайте Isabelle есть учебник «Программирование и проверка» , который практически идентичен первой половине «Конкретной семантики».
Тем не менее, он сфокусирован на приложениях в области компьютерных наук.(семантика языков программирования и немного функционального программирования).Я не уверен, есть ли хорошее руководство о том, как делать математику в Изабель;в любом случае математику, как правило, труднее сделать в доказательстве теорем для начинающих, потому что разрыв с неформальными рассуждениями на бумаге больше.Поэтому я рекомендую «Конкретную семантику», даже если вы в конечном итоге заинтересованы в формализации математики.
Кстати: вы упомянули Isabelle2017, но на самом деле нет причин использовать ее вместо Isabelle2018, которая является самой последней версиейна момент написания этого ответа.