src/HOL/ex/Execute_Choice.thy
changeset 37380 35815ce9218a
parent 37055 8f9f3d61ca8c
child 37595 9591362629e3