src/HOL/ex/InductiveInvariant.thy
changeset 24665 e5bea50b9b89
parent 21404 eb85850d3eb7
child 32960 69916a850301
equal deleted inserted replaced
24664:4195de64fdb1 24665:e5bea50b9b89