src/HOL/NumberTheory/Finite2.thy
changeset 17401 9147c880ada6
parent 15402 97204f3b4705
child 18369 694ea14ab4f2