src/HOL/Library/While_Combinator.thy
changeset 24506 020db6ec334a
parent 23821 2acd9d79d855
child 27368 9f90ac19e32b