src/HOL/ex/InductiveInvariant.thy
changeset 17459 9a3925c07392
parent 17388 495c799df31d
child 19736 d8d0f8f51d69