src/HOL/ex/InductiveInvariant_examples.thy
changeset 41963 d8c3b26b3da4
parent 32960 69916a850301