[isabelle-dev] Number_Theory in ROOT
lp15 at cam.ac.uk
Wed Jan 29 15:15:28 CET 2014
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?
session "HOL-Number_Theory" in Number_Theory = HOL +
options [document = false]
session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL +
Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
Theorem, Wilson's Theorem, Quadratic Reciprocity.
theories [document = false]
More information about the isabelle-dev