isabelle: src/HOL/NumberTheory/ROOT.ML@0a3dace545c5 (annotated)

9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	1
11049 7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 9944 diff changeset	2	no_document use_thy "Permutation";
11368 9c1995c73383 tuned Primes theory; wenzelm parents: 11049 diff changeset	3	no_document use_thy "Primes";
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	4
11049 7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 9944 diff changeset	5	use_thy "Fib";
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 9944 diff changeset	6	use_thy "Factorization";
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 9944 diff changeset	7	use_thy "Chinese";
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 9944 diff changeset	8	use_thy "EulerFermat";
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";