Weyl's Das Kontinuum formalised in the proof assistant Plastic.
In 1918, Weyl wrote the book Das Kontinuum, which sets out a system for the foundations of mathematics that is both predicative and employs classical logic. To modern eyes, it reads like the definition of a logic-enriched type theory. Here, it is built as a logic-enriched type theory using the proof assistant Plastic, and many of the results from the book are proven.
Unfortunately, the proof assistant Plastic seems to be no longer readily available, and its source code is difficult to compile on modern systems. Its old homepage is here:
http://homepages.inf.ed.ac.uk/wadler/realworld/plastic.html
The formalisation is described in my paper "Weyl's Predicative Classical Mathematics as a Logic-Enriched Type Theory", available here: