src/HOL/Library/While_Combinator.thy
changeset 26928 ca87aff1ad2d
parent 23821 2acd9d79d855
child 27368 9f90ac19e32b