[isabelle-dev] Number_Theory in ROOT

[Lawrence Paulson]

I’m puzzled about the inconsistency between the treatment of the new and old number theory libraries in the file ROOT.

The old one is as I would expect, with a description and the loading of some antecedent theories with document output suppressed. The new one basically looks like a stub. Is this just an oversight?

Larry


session "HOL-Number_Theory" in Number_Theory = HOL +
  options [document = false]
  theories Number_Theory

session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL +
  description {*
    Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
    Theorem, Wilson's Theorem, Quadratic Reciprocity.
  *}
  options [document_graph]
  theories [document = false]
    "~~/src/HOL/Library/Infinite_Set"
    "~~/src/HOL/Library/Permutation"
  theories
    Fib
    Factorization
    Chinese
    WilsonRuss
    WilsonBij
    Quadratic_Reciprocity
    Primes
    Pocklington
  files "document/root.tex"