src/HOL/ex/InductiveInvariant_examples.thy
changeset 25913 e1b6521c1f94
parent 19769 c40ce2de2020
child 32960 69916a850301
equal deleted inserted replaced
25912:a1a3f614dd86 25913:e1b6521c1f94