src/HOL/Library/While_Combinator.thy
changeset 29539 abfe2af6883e
parent 27487 c8a6ce181805
child 30738 0842e906300c
equal deleted inserted replaced
29538:5cc98af1398d 29539:abfe2af6883e