src/HOL/NumberTheory/ROOT.ML
author paulson
Thu Aug 03 10:46:01 2000 +0200 (2000-08-03)
changeset 9508 4d01dbf6ded7
child 9944 2a705d1af4dc
permissions -rw-r--r--
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson@9508
     1
(*  Title:      HOL/NumberTheory/ROOT
paulson@9508
     2
    ID:         $Id$
paulson@9508
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@9508
     4
    Copyright   2000  University of Cambridge
paulson@9508
     5
paulson@9508
     6
Number theory developments by Thomas M Rasmussen
paulson@9508
     7
*)
paulson@9508
     8
paulson@9508
     9
use_thy "Chinese";
paulson@9508
    10
use_thy "EulerFermat";
paulson@9508
    11
use_thy "WilsonRuss";
paulson@9508
    12
use_thy "WilsonBij";