src/HOL/Number_Theory/Totient.thy
changeset 79524 a0174eeca5ce
parent 72671 588c751a5eef
child 82664 e9f3b94eb6a0
equal deleted inserted replaced
79523:f1287f1894a0 79524:a0174eeca5ce