doc-src/Main/Docs/ROOT.ML

beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
another consequence of the transition to FOF

use_thy "Main_Doc";