src/HOL/ex/InductiveInvariant_examples.thy
changeset 19635 f7aa7d174343
parent 19623 12e6cc4382ae
child 19769 c40ce2de2020