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
paulson@9508
     1
haftmann@32479
     2
no_document use_thys ["Infinite_Set", "Permutation"];
wenzelm@24104
     3
use_thys ["Fib", "Factorization", "Chinese", "WilsonRuss",
haftmann@32479
     4
  "WilsonBij", "Quadratic_Reciprocity", "Primes", "Pocklington"];