src/HOL/Library/While_Combinator.thy
changeset 11295 66925f23ac7f
parent 11284 981ea92a86dd
child 11549 e7265e70fd7c