src/HOL/Library/While_Combinator.thy
changeset 12770 bdd17e7b5bd9
parent 11914 bca734def300
child 12791 ccc0f45ad2c4
equal deleted inserted replaced
12769:0f70bfe510ee 12770:bdd17e7b5bd9