src/HOL/ex/InductiveInvariant_examples.thy
changeset 36348 89c54f51f55a
parent 32960 69916a850301