src/HOL/NumberTheory/ROOT.ML
author wenzelm
Mon, 13 May 2002 11:05:27 +0200
changeset 13142 1ebd8ed5a1a0
parent 11368 9c1995c73383
child 13871 26e5f5e624f6
permissions -rw-r--r--
tuned document;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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";