src/HOL/Library/While_Combinator.thy
changeset 80999 7f9e8516ca05
parent 74974 7733c794cfea
child 81347 31f9e5ada550
equal deleted inserted replaced
80998:3668aec7afa2 80999:7f9e8516ca05