src/HOL/IMP/OO.thy
changeset 82488 b52e57ed7e29
parent 80914 d97fdabd9e2b