src/HOL/ex/InductiveInvariant_examples.thy
changeset 40858 69ab03d29c92
parent 32960 69916a850301
equal deleted inserted replaced
40854:f2c9ebbe04aa 40858:69ab03d29c92