GitLab

This only adapts existing .thy files so that compilation go through.
Modifications may/(should?) be improved as they were mainly application of
sledgehammer.
Compilation should work for both Isabelle2016-1 and Isabelle2017.