src/HOL/While.thy
changeset 10246 d8c968e6329a
parent 9448 755330e55e18