src/HOL/ex/InductiveInvariant_examples.thy
changeset 33791 fef59343b4b3
parent 32960 69916a850301
equal deleted inserted replaced
33790:b2ff505e30f8 33791:fef59343b4b3