src/HOL/Library/While_Combinator.thy
changeset 26475 3cc1e48d0ce1
parent 23821 2acd9d79d855
child 27368 9f90ac19e32b