src/HOL/Library/While_Combinator.thy
changeset 61344 ebf296fe88d7
parent 61166 5976fe402824
child 61424 c3658c18b7bc