src/HOL/ex/Mutil.ML
changeset 1717 8d46452739d7
parent 1684 3eaf3ab53082
child 1820 e381e1c51689