src/HOL/Library/While_Combinator.thy
changeset 21889 682dbe947862
parent 21404 eb85850d3eb7
child 22803 5129e02f4df2