src/HOL/Library/While_Combinator.thy
changeset 35007 8c339c73495c
parent 30738 0842e906300c
child 37757 dc78d2d9e90a
equal deleted inserted replaced
34999:5312d2ffee3b 35007:8c339c73495c