src/HOL/Proofs/Lambda/ROOT.ML

fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left

no_document use_thys ["~~/src/HOL/Library/Code_Integer"];
use_thys ["Eta", "StrongNorm", "Standardization", "WeakNorm"];