src/HOL/ex/Execute_Choice.thy
changeset 49811 3fc6b3289c31
parent 44899 95a53c01ed61
child 49929 70300f1b6835