src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy
changeset 51085 d90218288d51
parent 48480 cb03acfae211
child 52046 bc01725d7918