src/HOL/Library/While_Combinator.thy
changeset 41737 1b225934c09d
parent 41720 f749155883d7
child 41764 5268aef2fe83