isabelle: src/HOL/NumberTheory/ROOT.ML@8ae6f7b0903b (annotated)

19671 e293e16d1442 removed outdated/redundant comments; wenzelm parents: 14271 diff changeset	1	(* $Id$ *)
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	2
20809 6c4fd0b4b63a moved theory Infinite_Set to Library; wenzelm parents: 19671 diff changeset	3	no_document use_thy "Infinite_Set";
11049 7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 9944 diff changeset	4	no_document use_thy "Permutation";
11368 9c1995c73383 tuned Primes theory; wenzelm parents: 11049 diff changeset	5	no_document use_thy "Primes";
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	6
11049 7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 9944 diff changeset	7	use_thy "Fib";
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 9944 diff changeset	8	use_thy "Factorization";
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 9944 diff changeset	9	use_thy "Chinese";
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 9944 diff changeset	10	use_thy "WilsonRuss";
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 9944 diff changeset	11	use_thy "WilsonBij";
13871 26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer paulson parents: 11368 diff changeset	12	use_thy "Quadratic_Reciprocity";

author	huffman
	Mon, 11 Jun 2007 02:24:39 +0200
changeset 23305	8ae6f7b0903b
parent 20809	6c4fd0b4b63a
child 24104	719fbe4fb77f
permissions	-rw-r--r--