(*<*) theory Incredible_Everything imports Incredible_Correctness Incredible_Completeness begin (* This file depends on all theory, to have a single entry point. *) (* It can be used to pretty-print Isabelle output into the proof document. This is not used at the moment. *) end (*>*)