isabelle: src/HOL/Number_Theory/Number_Theory.thy@59feb83c6ab9 (annotated)

32479 521cc9bf2958 some reorganization of number theory haftmann parents: diff changeset	1
60526 fad653acf58f isabelle update_cartouches; wenzelm parents: 58889 diff changeset	2	section \<open>Comprehensive number theory\<close>
32479 521cc9bf2958 some reorganization of number theory haftmann parents: diff changeset	3
521cc9bf2958 some reorganization of number theory haftmann parents: diff changeset	4	theory Number_Theory
66276 acc3b7dd0b21 More material on powers for HOL-Computational_Algebra/HOL-Number_Theory eberlm <eberlm@in.tum.de> parents: 64318 diff changeset	5	imports Fib Residues Eratosthenes Quadratic_Reciprocity Pocklington Prime_Powers
32479 521cc9bf2958 some reorganization of number theory haftmann parents: diff changeset	6	begin
521cc9bf2958 some reorganization of number theory haftmann parents: diff changeset	7
521cc9bf2958 some reorganization of number theory haftmann parents: diff changeset	8	end
51173 3cbb4e95a565 Sieve of Eratosthenes haftmann parents: 32479 diff changeset	9