src/HOL/While.ML
changeset 10168 50be659d4222
parent 9747 043098ba5098
child 10186 499637e8f2c6