src/HOL/While.ML
changeset 9955 6ed42bcba707
parent 9747 043098ba5098
child 10186 499637e8f2c6