src/HOL/Library/While_Combinator.thy
changeset 32657 5f13912245ff
parent 30738 0842e906300c
child 37757 dc78d2d9e90a
equal deleted inserted replaced
32653:7feb35deb6f6 32657:5f13912245ff