src/HOL/Library/While_Combinator.thy
changeset 25767 852bce03412a
parent 23821 2acd9d79d855
child 27368 9f90ac19e32b