src/HOL/ex/InductiveInvariant.thy
changeset 38587 1317657d6aa9
parent 32960 69916a850301
child 44013 5cfc1c36ae97
equal deleted inserted replaced
38586:09fe051f2782 38587:1317657d6aa9