src/HOL/ex/Execute_Choice.thy
changeset 37407 61dd8c145da7
parent 37055 8f9f3d61ca8c
child 37595 9591362629e3
equal deleted inserted replaced
37406:982f3e02f3c4 37407:61dd8c145da7