src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy
changeset 60299 5ae2a2e74c93
parent 58889 5b7a9633cfa8
child 61670 301e0b4ecd45