src/HOL/Library/While_Combinator.thy
changeset 29401 94fd5dd918f5
parent 27487 c8a6ce181805
child 30738 0842e906300c
equal deleted inserted replaced
29374:ff4ba1ed4527 29401:94fd5dd918f5