src/HOL/ex/InductiveInvariant.thy
changeset 17780 274eaa114c6d
parent 17388 495c799df31d
child 19736 d8d0f8f51d69
equal deleted inserted replaced
17779:407bea05c2da 17780:274eaa114c6d