src/HOL/Number_Theory/Number_Theory.thy
author wenzelm
Wed, 19 May 2021 11:54:58 +0200
changeset 73740 c46ff0efa1ce
parent 69790 154cf64e403e
child 82518 da14e77a48b2
permissions -rw-r--r--
more direct use of latex tools: avoid diversion into "isabelle latex -o pdf" and its confusion of ISABELLE_PDFLATEX vs. ISABELLE_LUALATEX; clarified ISABELLE_MAKEINDEX options;


section \<open>Comprehensive number theory\<close>

theory Number_Theory
imports
  Fib
  Residues
  Eratosthenes
  Mod_Exp
  Quadratic_Reciprocity
  Pocklington
  Prime_Powers
  Residue_Primitive_Roots
begin

end