src/HOL/ex/InductiveInvariant.thy
changeset 23318 6d68b07ab5cf
parent 21404 eb85850d3eb7
child 32960 69916a850301
equal deleted inserted replaced
23317:90be000da2a7 23318:6d68b07ab5cf