src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy
changeset 62337 d3996d5873dd
parent 61670 301e0b4ecd45