src/HOL/Lambda/ROOT.ML

Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.

Syntax.ambiguity_level := 100;
Proofterm.proofs := 2;

no_document use_thys ["Code_Integer"];
use_thys ["Eta", "StrongNorm", "Standardization", "WeakNorm"];