src/HOL/ex/Execute_Choice.thy
changeset 66447 a1f5c5c26fa6
parent 64267 b9a1486e79be
child 66453 cc19f7ca2ed6