src/HOL/ex/InductiveInvariant_examples.thy
changeset 22991 b9e2a133e84e
parent 19769 c40ce2de2020
child 32960 69916a850301
equal deleted inserted replaced
22990:775e9de3db48 22991:b9e2a133e84e