src/HOL/IMP/AbsInt0_fun.thy
changeset 45109 20b3377b08d7
parent 45015 fdac1e9880eb