The effect of the theorem prover Isabelle.

Isabelle/HOL is a generic proof assistant. Using an Isabelle/HOL requires insight into procedures as well as into the concepts involved. In addition, the way computer manages the procedures can affect mathematical concepts. We can clearly understand mathematical concepts and can minimize the burden of operation opportunities. "Foundations of Geometry" is a book of mathematics written by Hilbert in 1899. The book is famous as the most rigorous study of the axiom system of Euclidean geometry by axioms and formalism. The purpose of this paper is to complement the axiom system by theorizing a part of the problems in this book. [ABSTRACT FROM AUTHOR]