overview of finiteness proof Gerog comment "not helpful", adding more intuitions of "closed forms"
Theories:
=========
Lexer.thy
Simplifying.thy
The repository can be checked using Isabelle 2017.
isabelle build -c -v -d . Lex
isabelle build -c -v -d . Paper
isabelle build -c -v -d . Journal
Other directories are:
=====================
Paper
Journal
Literature