src/HOL/ex/Execute_Choice.thy
changeset 49890 89eff795f757
parent 44899 95a53c01ed61
child 49929 70300f1b6835