src/HOL/IMP/Collecting1.thy
changeset 46150 d6cafcc012ec
parent 46070 8392c28d7868
child 46334 3858dc8eabd8