src/HOL/ex/InductiveInvariant_examples.thy
changeset 44052 00f0c8782a51
parent 32960 69916a850301