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