src/HOL/Library/While_Combinator.thy
changeset 50516 ed6b40d15d1c
parent 50180 c6626861c31a
child 50577 cfbad2d08412