src/HOL/Library/While_Combinator.thy
changeset 41734 d92cc39097e6
parent 41720 f749155883d7
child 41764 5268aef2fe83
equal deleted inserted replaced
41733:775da08dae1b 41734:d92cc39097e6