src/HOL/Library/While_Combinator.thy
changeset 21524 7843e2fd14a9
parent 21404 eb85850d3eb7
child 22803 5129e02f4df2