src/HOL/ex/InductiveInvariant.thy
changeset 26114 53eb3ff08cce
parent 21404 eb85850d3eb7
child 32960 69916a850301
equal deleted inserted replaced
26113:ba5909699cc3 26114:53eb3ff08cce