isabelle: src/HOL/Number_Theory/Number_Theory.thy@1e92b5c35615 (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
64318 1e92b5c35615 Repaired LaTeX in HOL-Data_Structures eberlm <eberlm@in.tum.de> parents: 64282 diff changeset	5	imports Fib Residues Eratosthenes Quadratic_Reciprocity Pocklington
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