src/HOL/Library/While_Combinator.thy
changeset 11566 94d2d6531c57
parent 11549 e7265e70fd7c
child 11626 0dbfb578bf75