src/HOL/Library/While_Combinator.thy
changeset 30297 41957d25a8b6
parent 27487 c8a6ce181805
child 30738 0842e906300c