src/HOL/ex/InductiveInvariant_examples.thy
changeset 43958 bc5e767f0f46
parent 32960 69916a850301
equal deleted inserted replaced
43957:64f88ef1835e 43958:bc5e767f0f46