src/HOL/NumberTheory/Finite2.thy
changeset 17433 4cf2e7980529
parent 15402 97204f3b4705
child 18369 694ea14ab4f2