src/HOL/ex/Execute_Choice.thy
changeset 44262 355d5438f5fb
parent 44174 d1d79f0e1ea6
child 44899 95a53c01ed61