src/HOL/IMP/Collecting.thy
changeset 61790 0494964bb226
parent 61670 301e0b4ecd45
child 61890 f6ded81f5690