src/HOL/ex/Commands.thy
changeset 71216 e64c249d3d98
parent 70308 7f568724d67e