src/HOL/Finite.ML
changeset 7699 09d8fd81cc1f
parent 7499 23e090051cb8
child 7821 a8717f53036c