src/HOL/ex/Execute_Choice.thy
changeset 44525 fbb777aec0d4
parent 44174 d1d79f0e1ea6
child 44899 95a53c01ed61