src/HOL/Library/While_Combinator.thy
changeset 22495 c54748fd1f43
parent 21404 eb85850d3eb7
child 22803 5129e02f4df2
equal deleted inserted replaced
22494:b61306c7987a 22495:c54748fd1f43