src/HOL/Finite.ML
changeset 5479 5a5dfb0f0d7d
parent 5477 41ab0f44dd8f
child 5516 d80e9aeb4a2b