src/HOL/Library/While_Combinator.thy
changeset 41734 d92cc39097e6
parent 41720 f749155883d7
child 41764 5268aef2fe83