src/HOL/Library/While_Combinator.thy
changeset 50551 67d934cdc9b9
parent 50180 c6626861c31a
child 50577 cfbad2d08412