src/HOL/ex/InductiveInvariant.thy
changeset 16701 abd0abd66387
parent 16417 9bc16273c2d4
child 17388 495c799df31d
equal deleted inserted replaced
16700:92925e30ff59 16701:abd0abd66387