Session Mersenne_Primes

Theories

• HOL-Number_Theory.Fib
• HOL-Number_Theory.Cong
• HOL-Number_Theory.Totient
• HOL-Number_Theory.Residues
• HOL-Number_Theory.Eratosthenes
• HOL-Number_Theory.Mod_Exp
• HOL-Number_Theory.Euler_Criterion
• HOL-Number_Theory.Gauss
• HOL-Number_Theory.Quadratic_Reciprocity
• HOL-Number_Theory.Pocklington
• HOL-Number_Theory.Prime_Powers
• HOL-Number_Theory.Residue_Primitive_Roots
• HOL-Number_Theory.Number_Theory
• Probabilistic_Prime_Tests.Legendre_Symbol
• Probabilistic_Prime_Tests.Algebraic_Auxiliaries
• Probabilistic_Prime_Tests.Jacobi_Symbol
• Lucas_Lehmer_Auxiliary
• Pell.Pell
• Lucas_Lehmer
• Native_Word.Code_Int_Integer_Conversion
• Word_Lib.More_Arithmetic
• Word_Lib.More_Divides
• Word_Lib.More_Bit_Ring
• Word_Lib.More_Word
• Word_Lib.Bit_Shifts_Infix_Syntax
• Word_Lib.Most_significant_bit
• Word_Lib.Least_significant_bit
• Word_Lib.Generic_set_bit
• Word_Lib.Bit_Comprehension
• Native_Word.Code_Target_Integer_Bit
• Native_Word.Code_Target_Int_Bit
• Lucas_Lehmer_Code