src/HOL/Library/While_Combinator.thy
changeset 54381 9c1f21365326
parent 54050 48c800d8ba2d
child 54196 0c188a3c671a