src/HOL/Old_Number_Theory/ROOT.ML
author haftmann
Fri Nov 27 08:41:10 2009 +0100 (2009-11-27)
changeset 33963 977b94b64905
parent 32479 521cc9bf2958
child 41413 64cd30d6b0b8
permissions -rw-r--r--
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
     1 
     2 no_document use_thys ["Infinite_Set", "Permutation"];
     3 use_thys ["Fib", "Factorization", "Chinese", "WilsonRuss",
     4   "WilsonBij", "Quadratic_Reciprocity", "Primes", "Pocklington"];