src/HOL/Library/While_Combinator.thy
changeset 21889 682dbe947862
parent 21404 eb85850d3eb7
child 22803 5129e02f4df2
equal deleted inserted replaced
21888:c75a44597fb7 21889:682dbe947862