src/HOL/ex/InductiveInvariant.thy
changeset 39494 bf7dd4902321
parent 32960 69916a850301
child 44013 5cfc1c36ae97
equal deleted inserted replaced
39493:cb2208f2c07d 39494:bf7dd4902321