isabelle: src/HOL/NumberTheory/ROOT.ML@25b068a99d2b (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
11049 7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 9944 diff changeset	3	no_document use_thy "Permutation";
11368 9c1995c73383 tuned Primes theory; wenzelm parents: 11049 diff changeset	4	no_document use_thy "Primes";
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	5
11049 7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 9944 diff changeset	6	use_thy "Fib";
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 9944 diff changeset	7	use_thy "Factorization";
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 9944 diff changeset	8	use_thy "Chinese";
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 9944 diff changeset	9	use_thy "WilsonRuss";
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 9944 diff changeset	10	use_thy "WilsonBij";
13871 26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer paulson parents: 11368 diff changeset	11	use_thy "Quadratic_Reciprocity";

author	webertj
	Wed, 26 Jul 2006 19:23:04 +0200
changeset 20217	25b068a99d2b
parent 19671	e293e16d1442
child 20809	6c4fd0b4b63a
permissions	-rw-r--r--