src/HOL/ex/InductiveInvariant_examples.thy
changeset 30242 aea5d7fa7ef5
parent 19769 c40ce2de2020
child 32960 69916a850301
equal deleted inserted replaced
30241:3a1aef73b2b2 30242:aea5d7fa7ef5