src/HOL/Library/While_Combinator.thy
changeset 12125 316d11f760f7
parent 11914 bca734def300
child 12791 ccc0f45ad2c4