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