src/HOL/ex/InductiveInvariant_examples.thy
changeset 39133 70d3915c92f0
parent 32960 69916a850301
equal deleted inserted replaced
39132:ba17ca3acdd3 39133:70d3915c92f0