src/HOL/Lambda/ROOT.ML

 Syntax.ambiguity_level := 100;
-Proofterm.proofs := 2;
 
 no_document use_thys ["Code_Integer"];
 use_thys ["Eta", "StrongNorm", "Standardization", "WeakNorm"];