src/HOL/IMP/Abs_Int0_fun.thy
changeset 45840 dadd139192d1
parent 45655 a49f9428aba4
child 45903 02dd9319dcb7