src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy
changeset 55454 6ea67a791108
parent 52046 bc01725d7918
child 55601 b7f4da504b75